law mul_double_sym

bend-mathlib@0.8.1.0 · nat.bend:4819

import Base

4819# Multiplying by a doubled factor doubles the product: a * double b = double (a * b), reversed to rewrite toward the simple side.
4820law mul_double_sym:
4821  for a: Nat
4822  for b: Nat
4823  {Nat.double(Nat.mul(a, b)) == Nat.mul(a, Nat.double(b)) : Nat}