Let a be given.
Assume HaR: a ∈ R.
We will prove preimage_of R neg_fun (open_ray_upper R a) = open_ray_lower R (minus_SNo a).
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of R neg_fun (open_ray_upper R a).
We will prove t ∈ open_ray_lower R (minus_SNo a).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun neg_fun x0 ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim Himg: apply_fun neg_fun t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun neg_fun x0 ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim Hrel: order_rel R a (apply_fun neg_fun t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun neg_fun t) Himg).
We prove the intermediate claim Halt: Rlt a (apply_fun neg_fun t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun neg_fun t) Hrel).
We prove the intermediate claim HimgEq: apply_fun neg_fun t = minus_SNo t.
An exact proof term for the current goal is (neg_fun_apply t HtR).
We prove the intermediate claim Halt2: Rlt a (minus_SNo t).
rewrite the current goal using HimgEq (from right to left).
An exact proof term for the current goal is Halt.
We prove the intermediate claim Htlt: Rlt t (minus_SNo a).
An exact proof term for the current goal is (iffEL (Rlt a (minus_SNo t)) (Rlt t (minus_SNo a)) (neg_fun_flip_upper a t HaR HtR) Halt2).
We prove the intermediate claim Hrel2: order_rel R t (minus_SNo a).
An exact proof term for the current goal is (Rlt_implies_order_rel_R t (minus_SNo a) Htlt).
We prove the intermediate claim HmaR: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 (minus_SNo a)) t HtR Hrel2).
Let t be given.
Assume Ht: t ∈ open_ray_lower R (minus_SNo a).
We will prove t ∈ preimage_of R neg_fun (open_ray_upper R a).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 (minus_SNo a)) t Ht).
We prove the intermediate claim Hrel: order_rel R t (minus_SNo a).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 (minus_SNo a)) t Ht).
We prove the intermediate claim Htlt: Rlt t (minus_SNo a).
An exact proof term for the current goal is (order_rel_R_implies_Rlt t (minus_SNo a) Hrel).
We prove the intermediate claim Halt2: Rlt a (minus_SNo t).
An exact proof term for the current goal is (iffER (Rlt a (minus_SNo t)) (Rlt t (minus_SNo a)) (neg_fun_flip_upper a t HaR HtR) Htlt).
We prove the intermediate claim Hpredef: preimage_of R neg_fun (open_ray_upper R a) = {x0 ∈ R|apply_fun neg_fun x0 ∈ open_ray_upper R a}.
Use reflexivity.
rewrite the current goal using Hpredef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HtR.
We prove the intermediate claim HimgR: apply_fun neg_fun t ∈ R.
An exact proof term for the current goal is (neg_fun_value_in_R t HtR).
We prove the intermediate claim HimgEq: apply_fun neg_fun t = minus_SNo t.
An exact proof term for the current goal is (neg_fun_apply t HtR).
We prove the intermediate claim Halt: Rlt a (apply_fun neg_fun t).
rewrite the current goal using HimgEq (from left to right).
An exact proof term for the current goal is Halt2.
We prove the intermediate claim Hrel2: order_rel R a (apply_fun neg_fun t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun neg_fun t) Halt).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R a x0) (apply_fun neg_fun t) HimgR Hrel2).
∎