Let f and p be given.
Assume Hp: prime_nat p.
Apply nat_ind to the current goal.
Assume _.
rewrite the current goal using Pi_SNo_0 (from left to right).
Assume H1: divides_int p 1.
We will prove False.
An exact proof term for the current goal is prime_not_divides_int_1 p Hp H1.
Let n be given.
Assume Hn: nat_p n.
Assume IHn: (∀i ∈ n, f i ∈ int) → divides_int p (Pi_SNo f n) → ∃i ∈ n, divides_int p (f i).
Assume H1: ∀i ∈ ordsucc n, f i ∈ int.
rewrite the current goal using Pi_SNo_S f n Hn (from left to right).
Assume H2: divides_int p (Pi_SNo f n * f n).
We prove the intermediate claim L1: ∀i ∈ n, f i ∈ int.
Let i be given.
Assume Hi.
Apply H1 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: f n ∈ int.
Apply H1 to the current goal.
Apply ordsuccI2 to the current goal.
Apply Euclid_lemma p Hp (Pi_SNo f n) (Pi_SNo_In_int f n Hn L1) (f n) L2 H2 to the current goal.
Assume H3: divides_int p (Pi_SNo f n).
Apply IHn L1 H3 to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ n.
Assume H4: divides_int p (f i).
We use i to witness the existential quantifier.
Apply andI 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.
An exact proof term for the current goal is H4.
Assume H3: divides_int p (f n).
We use n to witness the existential quantifier.
Apply andI to the current goal.
We will prove n ∈ ordsucc n.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is H3.
∎