We will prove 2 ∈ rational.
We prove the intermediate claim H2omega: 2 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 2 nat_2).
We prove the intermediate claim H2SNoS: 2 ∈ SNoS_ ω.
An exact proof term for the current goal is (omega_SNoS_omega 2 H2omega).
We prove the intermediate claim H2real: 2 ∈ real.
An exact proof term for the current goal is (SNoS_omega_real 2 H2SNoS).
We prove the intermediate claim H2int: 2 ∈ int.
An exact proof term for the current goal is (Subq_omega_int 2 H2omega).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim H1not0: 1 ∉ {0}.
Assume H1: 1 ∈ {0}.
We will prove False.
We prove the intermediate claim Heq: 1 = 0.
An exact proof term for the current goal is (SingE 0 1 H1).
An exact proof term for the current goal is (neq_1_0 Heq).
We prove the intermediate claim H1nonzero: 1 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} 1 H1omega H1not0).
We prove the intermediate claim Hrecip1: recip_SNo 1 = 1.
We prove the intermediate claim H1neq0: 1 ≠ 0.
An exact proof term for the current goal is neq_1_0.
We prove the intermediate claim Hinv: mul_SNo 1 (recip_SNo 1) = 1.
An exact proof term for the current goal is (recip_SNo_invR 1 SNo_1 H1neq0).
rewrite the current goal using (mul_SNo_oneL (recip_SNo 1) (SNo_recip_SNo 1 SNo_1)) (from right to left) at position 1.
An exact proof term for the current goal is Hinv.
We prove the intermediate claim Heq2: 2 = div_SNo 2 1.
We prove the intermediate claim Hdivdef: div_SNo 2 1 = mul_SNo 2 (recip_SNo 1).
Use reflexivity.
rewrite the current goal using Hdivdef (from left to right).
rewrite the current goal using Hrecip1 (from left to right).
rewrite the current goal using (mul_SNo_oneR 2 SNo_2) (from left to right).
Use reflexivity.
We prove the intermediate claim Hex: ∃m ∈ int, ∃n ∈ ω ∖ {0}, 2 = div_SNo m n.
We use 2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H2int.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1nonzero.
An exact proof term for the current goal is Heq2.
An exact proof term for the current goal is (SepI real (λx : set ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, x = div_SNo m n) 2 H2real Hex).
∎