law succ_add_sym

bend-mathlib@0.8.1.0 · nat.bend:3856

import Base

3856# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
3857law succ_add_sym:
3858  for -n: Nat
3859  for -m: Nat
3860  {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}