law add_right_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:3894

import Base

3894# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
3895law add_right_comm_sym:
3896  for a: Nat
3897  for b: Nat
3898  for c: Nat
3899  {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}