law two_mul_sym

bend-mathlib@0.8.1.0 · nat.bend:4785

import Base

4785# Two times n is n + n, reversed to rewrite toward the simple side.
4786law two_mul_sym:
4787  for n: Nat
4788  {Nat.add(n, n) == Nat.mul(2n, n) : Nat}