Let q be given.
Assume Hq.
Apply SepE real (λq ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, q = m :/: n) q Hq to the current goal.
Assume HqR: q ∈ real.
Assume HqQ.
Apply HqQ to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ int.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω ∖ {0}.
Assume H1: q = m :/: n.
Apply setminusE ω {0} n Hn to the current goal.
Assume Hno: n ∈ ω.
Assume Hnnz: n ∉ {0}.
We prove the intermediate claim LqS: SNo q.
An exact proof term for the current goal is real_SNo q HqR.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is omega_SNo n Hno.
We prove the intermediate claim LmqR: - q ∈ real.
An exact proof term for the current goal is real_minus_SNo q HqR.
We prove the intermediate claim LmqS: SNo (- q).
An exact proof term for the current goal is real_SNo (- q) LmqR.
We prove the intermediate claim LmqQ: ∃m ∈ int, ∃n ∈ ω ∖ {0}, - q = m :/: n.
We use (- m) to witness the existential quantifier.
We prove the intermediate claim LmmZ: - m ∈ int.
An exact proof term for the current goal is int_minus_SNo m Hm.
We prove the intermediate claim LmmS: SNo (- m).
An exact proof term for the current goal is int_SNo (- m) LmmZ.
We prove the intermediate claim LmmnS: SNo ((- m) :/: n).
An exact proof term for the current goal is SNo_div_SNo (- m) n ?? ??.
Apply andI to the current goal.
An exact proof term for the current goal is LmmZ.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
We will prove - q = (- m) :/: n.
We prove the intermediate claim Lnnz: n ≠ 0.
Assume H2: n = 0.
Apply Hnnz to the current goal.
We will prove n ∈ {0}.
rewrite the current goal using H2 (from left to right).
Apply SingI to the current goal.
Apply mul_SNo_nonzero_cancel_L n (- q) ((- m) :/: n) ?? ?? ?? ?? to the current goal.
We will prove n * (- q) = n * ((- m) :/: n).
Use transitivity with - (n * q), and - m.
We will prove n * (- q) = - (n * q).
An exact proof term for the current goal is mul_SNo_minus_distrR n q ?? ??.
We will prove - (n * q) = - m.
Use f_equal.
We will prove n * q = m.
rewrite the current goal using H1 (from left to right).
We will prove n * (m :/: n) = m.
An exact proof term for the current goal is mul_div_SNo_invR m n (int_SNo m Hm) ?? ??.
We will prove - m = n * ((- m) :/: n).
Use symmetry.
An exact proof term for the current goal is mul_div_SNo_invR (- m) n ?? ?? ??.
An exact proof term for the current goal is SepI real (λq ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, q = m :/: n) (- q) LmqR LmqQ.
∎