law add_assoc_sym

bend-mathlib@0.8.1.0 · nat.bend:3874

import Base

3874# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
3875law add_assoc_sym:
3876  for a: Nat
3877  for -b: Nat
3878  for -c: Nat
3879  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}