law add_cancel_r

lawful-words@0.1.0.0 · proof_nat.bend:289

import Base

289# x + a = y + a gives x = y.
290law add_cancel_r:
291  for +a: Nat
292  for +x: Nat
293  for +y: Nat
294  for e: {Nat.add(x, a) == Nat.add(y, a) : Nat}
295  {x == y : Nat}