law two_mul

bend-mathlib@0.8.1.0 · nat.bend:3535

import Base

3535# Two times n is n + n.
3536law two_mul:
3537  for n: Nat
3538  {Nat.mul(2n, n) == Nat.add(n, n) : Nat}