def ge_fin_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:60

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

60def ge_fin_zero(+c: Cmp, +x: Bool, +h: {Cmp.is_ge(c) == True{} : Bool}) -> {Cmp.is_ge(Word.cmp.fin(x, False{}, c)) == True{} : Bool}:
61  match c x:
62    case LT{} _:
63      Empty.absurd({Cmp.is_ge(Word.cmp.fin(x, False{}, LT{})) == True{} : Bool}, L.false_true(h))
64    case EQ{} True{}:
65      {==}
66    case EQ{} False{}:
67      {==}
68    case GT{} _:
69      {==}