law mul_double

bend-mathlib@0.8.1.0 · nat.bend:3582

import Base

3582# Multiplying by a doubled factor doubles the product: a * double b = double (a * b).
3583law mul_double:
3584  for a: Nat
3585  for b: Nat
3586  {Nat.mul(a, Nat.double(b)) == Nat.double(Nat.mul(a, b)) : Nat}