law successor_right

stelliferous@0.0.2.0 · proofs/natural_addition.bend:4

import Base

4law successor_right:
5  for +a: Nat
6  for +b: Nat
7  {Nat.add(a,1n+b) == 1n+Nat.add(a,b) : Nat}