~/jendhub

def cmp.lt_ne

bend-osdev-algo@0.1.0.0 · PROOF.bend:1000

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
import Base

1000def cmp.lt_ne(c: Cmp, e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_eq(c) == False{} : Bool}:
1001  match c:
1002    case LT{}:
1003      {==}
1004    case EQ{}:
1005      Empty.absurd({True{} == False{} : Bool}, absurd.ft(e))
1006    case GT{}:
1007      Empty.absurd({False{} == False{} : Bool}, absurd.ft(e))

Uses (6)

Used by (1)