Let p and q be given.
Assume Hp Hq Hpq.
Apply Hp to the current goal.
Assume H.
Apply H to the current goal.
Assume HpN: p ∈ ω.
Assume H1p: 1 ∈ p.
Assume Hpp: ∀k ∈ ω, divides_nat k p → k = 1 ∨ k = p.
Apply Hq to the current goal.
Assume H.
Apply H to the current goal.
Assume HqN: q ∈ ω.
Assume H1q: 1 ∈ q.
Assume Hqp: ∀k ∈ ω, divides_nat k q → k = 1 ∨ k = q.
We prove the intermediate claim L1: divides_nat p q.
Apply divides_int_divides_nat to the current goal.
An exact proof term for the current goal is HpN.
An exact proof term for the current goal is HqN.
An exact proof term for the current goal is Hpq.
Apply Hqp p HpN L1 to the current goal.
Assume H1: p = 1.
We will prove False.
Apply In_irref p to the current goal.
rewrite the current goal using H1 (from left to right) at position 1.
An exact proof term for the current goal is H1p.
Assume H1: p = q.
An exact proof term for the current goal is H1.
∎