def cancel_left

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/subtraction_bounds.bend:26

import Base

26def cancel_left(a: Nat, b: Nat, c: Nat, e: {Nat.add(a, b) == Nat.add(a, c) : Nat}) -> {b == c : Nat}:
27  match a:
28    case 0n: e
29    case 1n+p:
30      cancel_left(p, b, c, Equal.cong(Nat, Nat, predecessor, 1n+Nat.add(p, b), 1n+Nat.add(p, c), e))