law add_succ

bend-ml-nat-lemmas@0.1.2.0 · main.bend:41

import Base

41law add_succ:
42  for  a: Nat
43  for -b: Nat
44  {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}