def sub_le

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32half.bend:143

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

143# U32.sub is exact whenever the subtrahend is not larger (no borrow), so it
144# is the Nat subtraction of the two indices.
145def sub_le(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
146  match a b:
147    case a0 0n:
148      L.subst(Nat, z => {Nat.is_le(z, a0) == True{} : Bool}, a0, Nat.sub(a0, 0n), Equal.sym(Nat, Nat.sub(a0, 0n), a0, N.sub_zero(a0)), N.le_refl(a0))
149    case 0n 1n+q:
150      N.zero_le(Nat.sub(0n, 1n+q))
151    case 1n+p 1n+q:
152      N.le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), N.le_succ(p))