Let f be given.
Apply nat_ind to the current goal.
Assume _.
Let i be given.
Assume Hi: i ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE i Hi.
Let n be given.
Assume Hn: nat_p n.
Assume IHn: (∀i ∈ n, nat_p (f i)) → (∀i ∈ n, divides_nat (f i) (Pi_nat f n)).
Assume Hf: ∀i ∈ ordsucc n, nat_p (f i).
We prove the intermediate claim L1: ∀i ∈ n, nat_p (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: nat_p (Pi_nat f n).
An exact proof term for the current goal is Pi_nat_p f n Hn L1.
We prove the intermediate claim L3: nat_p (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_nat_S f n Hn (from left to right).
We will prove divides_nat (f i) (Pi_nat f n * f n).
Apply ordsuccE n i Hi to the current goal.
Assume H1: i ∈ n.
Apply divides_nat_tra (f i) (Pi_nat f n) to the current goal.
We will prove divides_nat (f i) (Pi_nat f n).
An exact proof term for the current goal is IHn L1 i H1.
We will prove divides_nat (Pi_nat f n) (Pi_nat f n * f n).
An exact proof term for the current goal is divides_nat_mulR (Pi_nat f n) (nat_p_omega (Pi_nat f n) L2) (f n) (nat_p_omega (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_nat f n * f n).
An exact proof term for the current goal is divides_nat_mulL (Pi_nat f n) (nat_p_omega (Pi_nat f n) L2) (f n) (nat_p_omega (f n) L3).
∎