law add_one

lawful-words@0.1.0.0 · proof_nat.bend:210

import Base

210law add_one:
211  for +n: Nat
212  {Nat.add(n, 1n) == 1n+n : Nat}