Assume _.

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

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_1.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: (∀i ∈ n, f i ∈ ω) → Pi_SNo f n ∈ ω.

Assume Hf: ∀i ∈ ordsucc n, f i ∈ ω.

We will prove Pi_SNo f (ordsucc n) ∈ ω.

rewrite the current goal using Pi_SNo_S f n Hn (from left to right).

We will prove Pi_SNo f n * f n ∈ ω.

Apply mul_SNo_In_omega to the current goal.

Apply IHn to the current goal.

Let i be given.

Assume Hi: i ∈ n.

We will prove 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 f n ∈ ω.

Apply Hf to the current goal.

We will prove n ∈ ordsucc n.

Apply ordsuccI2 to the current goal.