law double_mul_sym

bend-mathlib@0.8.1.0 · nat.bend:4810

import Base

4810# Doubling a product doubles its left factor: double (a * b) = double a * b, reversed to rewrite toward the simple side.
4811law double_mul_sym:
4812  for a: Nat
4813  for b: Nat
4814  {Nat.mul(Nat.double(a), b) == Nat.double(Nat.mul(a, b)) : Nat}