law double_mul

bend-mathlib@0.8.1.0 · nat.bend:3569

import Base

3569# Doubling a product doubles its left factor: double (a * b) = double a * b.
3570law double_mul:
3571  for a: Nat
3572  for b: Nat
3573  {Nat.double(Nat.mul(a, b)) == Nat.mul(Nat.double(a), b) : Nat}