Let p be given.

Assume Hp.

Assume H1: divides_int p 1.

Apply Hp to the current goal.

Assume H.

Apply H to the current goal.

Assume Hp1: p ∈ ω.

Assume Hp2: 1 ∈ p.

Assume _.

We prove the intermediate claim LpN: nat_p p.

An exact proof term for the current goal is omega_nat_p p Hp1.

We prove the intermediate claim Lpo: ordinal p.

An exact proof term for the current goal is nat_p_ordinal p LpN.

We prove the intermediate claim LpS: SNo p.

An exact proof term for the current goal is nat_p_SNo p LpN.

Apply SNoLt_irref 1 to the current goal.

We will prove 1 < 1.

Apply SNoLtLe_tra 1 p 1 SNo_1 LpS SNo_1 to the current goal.

We will prove 1 < p.

Apply ordinal_In_SNoLt p Lpo 1 to the current goal.

We will prove 1 ∈ p.

An exact proof term for the current goal is Hp2.

We will prove p ≤ 1.

An exact proof term for the current goal is divides_int_pos_Le p 1 H1 SNoLt_0_1.

∎