def nle

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:648

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

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