law add_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:3865

import Base

3865# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
3866law add_comm_sym:
3867  for n: Nat
3868  for m: Nat
3869  {Nat.add(m, n) == Nat.add(n, m) : Nat}