law successor_width

stelliferous@0.0.2.0 · proofs/natural_addition.bend:42

import Base

42law successor_width:
43  for +width: Nat
44  {Nat.add(width,1n) == 1n+width : Nat}