def nle

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:649

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

649def nle(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Bool.not(c) == Nat.is_le(b, a) : Bool}:
650  match c:
651    case True{}:
652      Equal.sym(Bool, Nat.is_le(b, a), False{}, N.lt_not_le(a, b, hc))
653    case False{}:
654      Equal.sym(Bool, Nat.is_le(b, a), True{}, N.not_lt_le(a, b, hc))