Let f be given.
Apply nat_ind to the current goal.
Assume _.
rewrite the current goal using Pi_SNo_0 (from left to right).
Apply Subq_omega_int to the current goal.
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 ∈ int) → Pi_SNo f n ∈ int.
Assume Hf: ∀i ∈ ordsucc n, f i ∈ int.
We will prove Pi_SNo f (ordsucc n) ∈ int.
rewrite the current goal using Pi_SNo_S f n Hn (from left to right).
We will prove Pi_SNo f n * f n ∈ int.
Apply int_mul_SNo to the current goal.
Apply IHn to the current goal.
Let i be given.
Assume Hi: i ∈ n.
We will prove f i ∈ int.
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 ∈ int.
Apply Hf to the current goal.
We will prove n ∈ ordsucc n.
Apply ordsuccI2 to the current goal.
∎