law add_left_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:3884

import Base

3884# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
3885law add_left_comm_sym:
3886  for a: Nat
3887  for b: Nat
3888  for -c: Nat
3889  {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}