def comparison_less_not_equal

stelliferous@0.0.2.0 · proofs/nat_order.bend:105

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

105def comparison_less_not_equal(+comparison: Cmp,less: {Cmp.is_lt(comparison) == True{} : Bool}) -> {Cmp.is_eq(comparison) == False{} : Bool}:
106  match comparison:
107    case LT{}: {==}
108    case EQ{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(less))
109    case GT{}: Empty.absurd({False{} == False{} : Bool},WordEncoding.false_true(less))