law add_right_cancel

bend-mathlib@0.8.1.0 · nat.bend:191

import Base

191# Addition cancels on the right: a + b = c + b implies a = c.
192law add_right_cancel:
193  for a: Nat
194  for b: Nat
195  for c: Nat
196  for e: {Nat.add(a, b) == Nat.add(c, b) : Nat}
197  {a == c : Nat}