law add_succ_right

bend-prot@0.1.0.0 · LAWS.bend:327

import Base

327# Adding a successor on the right pulls out front.
328law add_succ_right:
329  for b: Nat
330  for a: Nat
331  {Nat.add(b, 1n+a) == 1n+Nat.add(b, a) : Nat}