~/jendhub

def cm.not_le_flip

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

import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder
import Base

125def cm.not_le_flip(c: Cmp, +e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_le(cm.flip(c)) == False{} : Bool}:
126  match c:
127    case LT{}:
128      {==}
129    case EQ{}:
130      Empty.absurd({True{} == False{} : Bool}, ab.ft(e))
131    case GT{}:
132      Empty.absurd({True{} == False{} : Bool}, ab.ft(e))

Uses (7)

Used by (1)