law succ_add

bend-mathlib@0.8.1.0 · nat.bend:40

import Base

40# Adding a successor on the left: (n + 1) + m = (n + m) + 1.
41law succ_add:
42  for -n: Nat
43  for -m: Nat
44  {Nat.add(1n+n, m) == 1n+Nat.add(n, m) : Nat}