def sub_le2

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/arith.bend:168

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

168# a - b <= a
169def sub_le2(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
170  match a b:
171    case 0n _:
172      %Equal.sym(Nat, Nat.sub(0n, b), 0n, zsub(b)) : {Nat.is_le(_, 0n) == True{} : Bool}
173      {==}
174    case 1n+p 0n:
175      N.le_refl(1n+p)
176    case 1n+p 1n+q:
177      N.le_trans(Nat.sub(p, q), p, 1n+p, sub_le2(p, q), N.le_succ(p))