We will prove 1 ∈ rational.
We prove the intermediate claim H1real: 1 ∈ real.
An exact proof term for the current goal is real_1.
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 H1int: 1 ∈ int.
An exact proof term for the current goal is (Subq_omega_int 1 H1omega).
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 Heq1: 1 = div_SNo 1 1.
We prove the intermediate claim Hdivdef: div_SNo 1 1 = mul_SNo 1 (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 1 SNo_1) (from left to right).
Use reflexivity.
We prove the intermediate claim Hex: ∃m ∈ int, ∃n ∈ ω ∖ {0}, 1 = div_SNo m n.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1int.
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 Heq1.
An exact proof term for the current goal is (SepI real (λx : set ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, x = div_SNo m n) 1 H1real Hex).
∎