law mul_dbl_r

lawful-words@0.1.0.0 · proof_nat.bend:530

import Base

530law mul_dbl_r:
531  for +a: Nat
532  for +x: Nat
533  {Nat.mul(a, Nat.double(x)) == Nat.double(Nat.mul(a, x)) : Nat}