Let n be given.
Assume Hn: nat_p n.
Apply nat_ind to the current goal.
We will prove nat_p (n * 0).
rewrite the current goal using (mul_nat_0R n) (from left to right).
We will prove nat_p 0.
An exact proof term for the current goal is nat_0.
Let m be given.
Assume Hm: nat_p m.
Assume IHm: nat_p (n * m).
We will prove nat_p (n * ordsucc m).
rewrite the current goal using (mul_nat_SR n m Hm) (from left to right).
We will prove nat_p (n + n * m).
An exact proof term for the current goal is (add_nat_p n Hn (n * m) IHm).
∎