def sub_le_self

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:181

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

181def sub_le_self(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}:
182  match a b:
183    case 0n 0n:
184      {==}
185    case 0n 1n+ +bp:
186      {==}
187    case 1n+ +ap 0n:
188      N.le_refl(1n+ap)
189    case 1n+ +ap 1n+ +bp:
190      N.le_trans(Nat.sub(ap, bp), ap, 1n+ap, sub_le_self(ap, bp), N.le_succ(ap))