law nat_add_succ

bend-osdev-u32@0.1.0.0 · LAWS.bend:235

import Base

235law nat_add_succ:
236  for +x: Nat
237  for +y: Nat
238  {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}