~/jendhub

def cm.not_lt_flip

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

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

134def cm.not_lt_flip(c: Cmp, +e: {Cmp.is_le(c) == True{} : Bool}) -> {Cmp.is_lt(cm.flip(c)) == False{} : Bool}:
135  match c:
136    case LT{}:
137      {==}
138    case EQ{}:
139      {==}
140    case GT{}:
141      Empty.absurd({True{} == False{} : Bool}, ab.ft(e))

Uses (7)

Used by (1)