def le_c

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:121

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

121# is_lt(a, b) is is_le(a + 1, b)
122def le_c(+a: Nat, +b: Nat, +d: Bool, +hd: {Nat.is_le(1n+a, b) == d : Bool}, +hc: {Nat.is_lt(a, b) == False{} : Bool}) -> {False{} == d : Bool}:
123  match d:
124    case False{}:
125      {==}
126    case True{}:
127      Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_lt(a, b), False{}, Equal.sym(Bool, Nat.is_lt(a, b), True{}, N.succ_le_lt(a, b, hd)), hc)))