law add_succ_sym

bend-mathlib@0.8.1.0 · nat.bend:3847

import Base

3847# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
3848law add_succ_sym:
3849  for n: Nat
3850  for -m: Nat
3851  {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}