Assume H2: ¬ composite_nat n.

Apply orIL to the current goal.

We will prove n ∈ ω ∧ 1 ∈ n ∧ ∀k ∈ ω, divides_nat k n → k = 1 ∨ k = n.

Apply and3I to the current goal.

An exact proof term for the current goal is Hn.

An exact proof term for the current goal is H1.

Let k be given.

Assume Hk.

Assume Hkn: divides_nat k n.

Apply Hkn to the current goal.

Assume _ H.

Apply H to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume Hm: m ∈ ω.

Assume Hkm: k * m = n.

We will prove k = 1 ∨ k = n.

Apply dneg to the current goal.

Assume H3: ¬ (k = 1 ∨ k = n).

We prove the intermediate claim L1k: 1 ∈ k.

Apply ordinal_In_Or_Subq 1 k (nat_p_ordinal 1 nat_1) (nat_p_ordinal k (omega_nat_p k Hk)) to the current goal.

Assume H4: 1 ∈ k.

An exact proof term for the current goal is H4.

Assume H4: k ⊆ 1.

We will prove False.

Apply nat_le1_cases k (omega_nat_p k Hk) H4 to the current goal.

Assume H4: k = 0.

We prove the intermediate claim Ln0: n = 0.

Use transitivity with and k * m.

We will prove n = k * m.

Use symmetry.

An exact proof term for the current goal is Hkm.

We will prove k * m = 0.

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

We will prove 0 * m = 0.

An exact proof term for the current goal is mul_nat_0L m (omega_nat_p m Hm).

Apply In_no2cycle 0 1 In_0_1 to the current goal.

We will prove 1 ∈ 0.

rewrite the current goal using Ln0 (from right to left) at position 2.

An exact proof term for the current goal is H1.

Assume H4: k = 1.

Apply H3 to the current goal.

Apply orIL to the current goal.

An exact proof term for the current goal is H4.

We prove the intermediate claim L1m: 1 ∈ m.

Apply ordinal_In_Or_Subq 1 m (nat_p_ordinal 1 nat_1) (nat_p_ordinal m (omega_nat_p m Hm)) to the current goal.

Assume H4: 1 ∈ m.

An exact proof term for the current goal is H4.

Assume H4: m ⊆ 1.

We will prove False.

Apply nat_le1_cases m (omega_nat_p m Hm) H4 to the current goal.

Assume H4: m = 0.

We prove the intermediate claim Ln0: n = 0.

Use transitivity with and k * m.

We will prove n = k * m.

Use symmetry.

An exact proof term for the current goal is Hkm.

We will prove k * m = 0.

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

We will prove k * 0 = 0.

An exact proof term for the current goal is mul_nat_0R k.

Apply In_no2cycle 0 1 In_0_1 to the current goal.

We will prove 1 ∈ 0.

rewrite the current goal using Ln0 (from right to left) at position 2.

An exact proof term for the current goal is H1.

Assume H4: m = 1.

Apply H3 to the current goal.

Apply orIR to the current goal.

We will prove k = n.

Use transitivity with and k * m.

We will prove k = k * m.

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

Use symmetry.

An exact proof term for the current goal is mul_nat_1R k.

We will prove k * m = n.

An exact proof term for the current goal is Hkm.

Apply H2 to the current goal.

We will prove composite_nat n.

We will prove n ∈ ω ∧ ∃k m ∈ ω, 1 ∈ k ∧ 1 ∈ m ∧ k * m = n.

Apply andI to the current goal.

An exact proof term for the current goal is Hn.

We use k to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hk.

We use m to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hm.

We will prove 1 ∈ k ∧ 1 ∈ m ∧ k * m = n.

Apply and3I to the current goal.

An exact proof term for the current goal is L1k.

An exact proof term for the current goal is L1m.

An exact proof term for the current goal is Hkm.