law mul_succ_r

lawful-words@0.1.0.0 · proof_nat.bend:396

import Base

396law mul_succ_r:
397  for +a: Nat
398  for +b: Nat
399  {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}