law double_eq_two_mul_sym

bend-mathlib@0.8.1.0 · nat.bend:4793

import Base

4793# Doubling is multiplying by two: double n = 2 * n, reversed to rewrite toward the simple side.
4794law double_eq_two_mul_sym:
4795  for n: Nat
4796  {Nat.mul(2n, n) == Nat.double(n) : Nat}