Let m be given.

Assume Hm.

Apply setminusE ω {0} m Hm to the current goal.

Assume Hm1: m ∈ ω.

Assume Hm2: m ∉ {0}.

We prove the intermediate claim LmZ: m ∈ int.

Apply Subq_omega_int to the current goal.

An exact proof term for the current goal is Hm1.

Apply gcd_id m Hm to the current goal.

Assume H.

Apply H to the current goal.

Assume _.

Assume H1: divides_int m m.

Assume H2: ∀d', divides_int d' m → divides_int d' m → d' ≤ m.

We will prove divides_int m 0 ∧ divides_int m m ∧ ∀d', divides_int d' 0 → divides_int d' m → d' ≤ m.

Apply and3I to the current goal.

We will prove divides_int m 0.

Apply divides_int_0 to the current goal.

We will prove m ∈ int.

An exact proof term for the current goal is LmZ.

We will prove divides_int m m.

An exact proof term for the current goal is H1.

Let d' be given.

Assume H3: divides_int d' 0.

Assume H4: divides_int d' m.

We will prove d' ≤ m.

Apply H2 to the current goal.

An exact proof term for the current goal is H4.

∎