Assume H1: composite_nat n.

Apply H1 to the current goal.

Assume _ H.

Apply H to the current goal.

Let k be given.

Assume H.

Apply H to the current goal.

Assume Hk: k ∈ ω.

Assume H.

Apply H to the current goal.

Let m be given.

Assume H.

Apply H to the current goal.

Assume Hm: m ∈ ω.

Assume H.

Apply H to the current goal.

Assume H.

Apply H to the current goal.

Assume H1k: 1 ∈ k.

Assume H1m: 1 ∈ m.

Assume Hkm: k * m = n.

We prove the intermediate claim Lk: k ∈ n.

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

We will prove k ∈ k * m.

Apply mul_nat_0m_1n_In k (omega_nat_p k Hk) m (omega_nat_p m Hm) to the current goal.

We will prove 0 ∈ k.

Apply nat_trans k (omega_nat_p k Hk) 1 H1k 0 In_0_1 to the current goal.

We will prove 1 ∈ m.

An exact proof term for the current goal is H1m.

Apply IHn k Lk H1k to the current goal.

Let p be given.

Assume H.

Apply H to the current goal.

Assume Hp: prime_nat p.

Assume Hpk: divides_nat p k.

We use p to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hp.

We will prove divides_nat p n.

Apply divides_nat_tra p k n Hpk to the current goal.

We will prove divides_nat k n.

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

We will prove divides_nat k (k * m).

Apply divides_nat_mulR to the current goal.

We will prove k ∈ ω.

An exact proof term for the current goal is Hk.

We will prove m ∈ ω.

An exact proof term for the current goal is Hm.