law add_succ

bend-mathlib@0.8.1.0 · nat.bend:26

import Base

26# Adding a successor on the right: n + (m + 1) = (n + m) + 1.
27law add_succ:
28  for n: Nat
29  for -m: Nat
30  {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}