def sub_le_self
bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/fact.bend:226
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend as Fact
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R
226def sub_le_self(+n: Nat, +k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
227 match n k:
228 case 0n k0:
229 %Equal.sym(Nat, Nat.sub(0n, k0), 0n, R.zsub(k0)) : {Nat.is_le(_, 0n) == True{} : Bool}
230 {==}
231 case 1n+ +np 0n:
232 N.le_refl(1n+np)
233 case 1n+ +np 1n+ +kp:
234 N.le_trans(Nat.sub(np, kp), np, 1n+np, sub_le_self(np, kp), N.le_succ(np))