law double_eq_two_mul

bend-mathlib@0.8.1.0 · nat.bend:3545

import Base

3545# Doubling is multiplying by two: double n = 2 * n.
3546law double_eq_two_mul:
3547  for n: Nat
3548  {Nat.double(n) == Nat.mul(2n, n) : Nat}