We will prove 2 ∈ ω ∧ 1 ∈ 2 ∧ ∀k ∈ ω, divides_nat k 2 → k = 1 ∨ k = 2.
Apply and3I to the current goal.
We will prove 2 ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_2.
An exact proof term for the current goal is In_1_2.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hk2: divides_nat k 2.
We will prove k = 1 ∨ k = 2.
Apply Hk2 to the current goal.
Assume _.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Assume Hkn: k * n = 2.
An exact proof term for the current goal is prime_nat_2_lem k (omega_nat_p k Hk) n (omega_nat_p n Hn) Hkn.
∎