law add_left_cancel

bend-mathlib@0.8.1.0 · nat.bend:176

import Base

176# Addition cancels on the left: a + b = a + c implies b = c.
177law add_left_cancel:
178  for a: Nat
179  for -b: Nat
180  for -c: Nat
181  for e: {Nat.add(a, b) == Nat.add(a, c) : Nat}
182  {b == c : Nat}