def cm.le_flip

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

import Base

106# flipping turns not-less into at-most and the other way
107def cm.le_flip(c: Cmp, +e: {Cmp.is_lt(c) == False{} : Bool}) -> {Cmp.is_le(cm.flip(c)) == True{} : Bool}:
108  match c:
109    case LT{}:
110      Empty.absurd({False{} == True{} : Bool}, ab.tf(e))
111    case EQ{}:
112      {==}
113    case GT{}:
114      {==}