def sub_cancel_l

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/arith.bend:97

import Base

97def sub_cancel_l(+c: Nat, +a: Nat, +b: Nat) -> {Nat.sub(Nat.add(c, a), Nat.add(c, b)) == Nat.sub(a, b) : Nat}:
98  match c:
99    case 0n:
100      {==}
101    case 1n+ +cp:
102      sub_cancel_l(cp, a, b)