Let n be given.
Assume Hn: nat_p n.
Let m be given.
Assume Hm: nat_p m.
Apply nat_ind to the current goal.
We will prove (n * m) * 0 = n * (m * 0).
rewrite the current goal using mul_nat_0R (from left to right) at position 2.
rewrite the current goal using mul_nat_0R (from left to right) at position 2.
An exact proof term for the current goal is (mul_nat_0R (n * m)).
Let k be given.
Assume Hk: nat_p k.
Assume IHk: (n * m) * k = n * (m * k).
We will prove (n * m) * ordsucc k = n * (m * ordsucc k).
rewrite the current goal using mul_nat_SR (from left to right).
We will prove n * m + (n * m) * k = n * (m * ordsucc k).
rewrite the current goal using mul_nat_SR (from left to right).
We will prove n * m + (n * m) * k = n * (m + m * k).
rewrite the current goal using mul_add_nat_distrL (from left to right).
We will prove n * m + (n * m) * k = n * m + n * (m * k).
rewrite the current goal using IHk (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hm.
An exact proof term for the current goal is (mul_nat_p m Hm k Hk).
An exact proof term for the current goal is Hk.
An exact proof term for the current goal is Hk.
∎