law add_comm

bend-mathlib@0.8.1.0 · nat.bend:49

import Base

49# Addition is commutative: n + m = m + n.
50law add_comm:
51  for n: Nat
52  for m: Nat
53  {Nat.add(n, m) == Nat.add(m, n) : Nat}