We will prove 0 ∈ rational.
We prove the intermediate claim H0real: 0 ∈ real.
An exact proof term for the current goal is real_0.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H0int: 0 ∈ int.
An exact proof term for the current goal is (Subq_omega_int 0 H0omega).
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 Heq0: 0 = div_SNo 0 1.
We prove the intermediate claim Hdiv: div_SNo 0 1 = 0.
An exact proof term for the current goal is (div_SNo_0_num 1 SNo_1).
rewrite the current goal using Hdiv (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hex: ∃m ∈ int, ∃n ∈ ω ∖ {0}, 0 = div_SNo m n.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H0int.
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 Heq0.
An exact proof term for the current goal is (SepI real (λx : set ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, x = div_SNo m n) 0 H0real Hex).
∎