law add_add_add_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:3904

import Base

3904# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
3905law add_add_add_comm_sym:
3906  for a: Nat
3907  for b: Nat
3908  for c: Nat
3909  for -d: Nat
3910  {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}