law mul2

lawful-words@0.1.0.0 · proof_nat.bend:514

import Base

514law mul2:
515  for +x: Nat
516  {Nat.mul(2n, x) == Nat.double(x) : Nat}