def sub_cancel_l

bend-collections-laws-math@1.0.0.0 · proofs/lib/arith.bend:136

import Base

136def sub_cancel_l(+c: Nat, +a: Nat, +b: Nat) -> {Nat.sub(Nat.add(c, a), Nat.add(c, b)) == Nat.sub(a, b) : Nat}:
137  match c:
138    case 0n:
139      {==}
140    case 1n+p:
141      sub_cancel_l(p, a, b)