Theorem: MyNat.mul_succ (NNG/MyNat/Multiplication.lean)

State before:
a b : ℕ
⊢ a * succ b = a * b + a
Tactic:
rfl
State after:
no goals