def cm.lt_flip

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:116

import Base

116def cm.lt_flip(c: Cmp, +e: {Cmp.is_le(c) == False{} : Bool}) -> {Cmp.is_lt(cm.flip(c)) == True{} : Bool}:
117  match c:
118    case LT{}:
119      Empty.absurd({False{} == True{} : Bool}, ab.tf(e))
120    case EQ{}:
121      Empty.absurd({False{} == True{} : Bool}, ab.tf(e))
122    case GT{}:
123      {==}