law add_right_comm

bend-mathlib@0.8.1.0 · nat.bend:103

import Base

103# Right commutativity of addition: (a + b) + c = (a + c) + b.
104law add_right_comm:
105  for a: Nat
106  for b: Nat
107  for c: Nat
108  {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}