Let m be given.
Assume Hm.
We prove the intermediate
claim LmZ:
m ∈ int.
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 _.
Apply and3I to the current goal.
An exact proof term for the current goal is LmZ.
An exact proof term for the current goal is H1.
Let d' be given.
Apply H2 to the current goal.
An exact proof term for the current goal is H4.
An exact proof term for the current goal is H4.
∎