law add_assoc

bend-mathlib@0.8.1.0 · nat.bend:71

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

71# Addition is associative: (a + b) + c = a + (b + c).
72law add_assoc:
73  for a: Nat
74  for -b: Nat
75  for -c: Nat
76  {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}

Uses (2)

Used by (13)