Let f be given.
Apply nat_ind to the current goal.
Assume _.
rewrite the current goal using Pi_nat_0 (from left to right).
An exact proof term for the current goal is nat_1.
Let n be given.
Assume Hn: nat_p n.
Assume IHn: (∀i ∈ n, nat_p (f i)) → nat_p (Pi_nat f n).
Assume Hf: ∀i ∈ ordsucc n, nat_p (f i).
We will prove nat_p (Pi_nat f (ordsucc n)).
rewrite the current goal using Pi_nat_S f n Hn (from left to right).
We will prove nat_p (Pi_nat f n * f n).
Apply mul_nat_p to the current goal.
Apply IHn to the current goal.
Let i be given.
Assume Hi: i ∈ n.
We will prove nat_p (f i).
Apply Hf to the current goal.
We will prove i ∈ ordsucc n.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We will prove nat_p (f n).
Apply Hf to the current goal.
We will prove n ∈ ordsucc n.
Apply ordsuccI2 to the current goal.
∎