Let n be given.

Assume Hn: nat_p n.

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

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

We prove the intermediate claim L1: ∀i ∈ n, f i ∈ ω.

Let i be given.

Assume Hi.

Apply Hf to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

We prove the intermediate claim L2: Pi_SNo f n ∈ ω.

An exact proof term for the current goal is Pi_SNo_In_omega f n Hn L1.

We prove the intermediate claim L3: f n ∈ ω.

Apply Hf to the current goal.

Apply ordsuccI2 to the current goal.

Let i be given.

Assume Hi: i ∈ ordsucc n.

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

We will prove divides_nat (f i) (Pi_SNo f n * f n).

Apply ordsuccE n i Hi to the current goal.

Assume H1: i ∈ n.

Apply divides_nat_tra (f i) (Pi_SNo f n) to the current goal.

We will prove divides_nat (f i) (Pi_SNo f n).

An exact proof term for the current goal is IHn L1 i H1.

We will prove divides_nat (Pi_SNo f n) (Pi_SNo f n * f n).

An exact proof term for the current goal is divides_nat_mul_SNo_R (Pi_SNo f n) L2 (f n) L3.

Assume H1: i = n.

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

We will prove divides_nat (f n) (Pi_SNo f n * f n).

An exact proof term for the current goal is divides_nat_mul_SNo_L (Pi_SNo f n) L2 (f n) L3.