law add_eq_zero_l

lawful-words@0.1.0.0 · proof_nat.bend:315

import Base

315# x + y = 0 gives x = 0 (and y = 0).
316law add_eq_zero_l:
317  for +x: Nat
318  for +y: Nat
319  for e: {Nat.add(x, y) == 0n : Nat}
320  {x == 0n : Nat}