Let n be given.

rewrite the current goal using mul_nat_SR n 0 nat_0 (from left to right).

We will prove n + n * 0 = n.

rewrite the current goal using mul_nat_0R (from left to right).

We will prove n + 0 = n.

Apply add_nat_0R to the current goal.

∎