law mul2_r

lawful-words@0.1.0.0 · proof_nat.bend:522

import Base

522law mul2_r:
523  for +x: Nat
524  {Nat.mul(x, 2n) == Nat.double(x) : Nat}