law mul_succ_r

minebender-game@1.0.0.0 · proof_base.bend:486

import Base

486law mul_succ_r:
487  for +a: Nat
488  for +b: Nat
489  {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}