law add_left_comm

bend-mathlib@0.8.1.0 · nat.bend:86

import Base

86# Left commutativity of addition: a + (b + c) = b + (a + c).
87law add_left_comm:
88  for a: Nat
89  for b: Nat
90  for -c: Nat
91  {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}