law mul_dbl_l

lawful-words@0.1.0.0 · proof_nat.bend:543

import Base

543law mul_dbl_l:
544  for +a: Nat
545  for +x: Nat
546  {Nat.mul(Nat.double(a), x) == Nat.double(Nat.mul(a, x)) : Nat}