def nle

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:192

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

192def nle(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Bool.not(c) == Nat.is_le(b, a) : Bool}:
193  match c:
194    case True{}:
195      Equal.sym(Bool, Nat.is_le(b, a), False{}, N.lt_not_le(a, b, hc))
196    case False{}:
197      Equal.sym(Bool, Nat.is_le(b, a), True{}, N.not_lt_le(a, b, hc))