def comparison_not_less

stelliferous@0.0.2.0 · proofs/nat_order.bend:98

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

98def comparison_not_less(+comparison: Cmp,h: {Cmp.is_lt(comparison) == False{} : Bool}) -> {Cmp.is_ge(comparison) == True{} : Bool}:
99  match comparison:
100    case LT{}:
101      Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},h)))
102    case EQ{}: {==}
103    case GT{}: {==}