Let c and a be given.
Assume HcR: c ∈ R.
Assume Hcpos: 0 < c.
Assume HaR: a ∈ R.
We will prove preimage_of R (mul_const_fun c) (open_ray_upper R a) = open_ray_upper R (div_SNo a c).
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R (mul_const_fun c) (open_ray_upper R a).
We will prove t ∈ open_ray_upper R (div_SNo a c).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun (mul_const_fun c) x0 ∈ open_ray_upper R a) t HtPre).
We prove the intermediate claim Himg: apply_fun (mul_const_fun c) t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun (mul_const_fun c) x0 ∈ open_ray_upper R a) t HtPre).
We prove the intermediate claim Hrel: order_rel R a (apply_fun (mul_const_fun c) t).
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ order_rel R a y0) (apply_fun (mul_const_fun c) t) Himg).
We prove the intermediate claim Halt: Rlt a (apply_fun (mul_const_fun c) t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun (mul_const_fun c) t) Hrel).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HmulEq: apply_fun (mul_const_fun c) t = mul_SNo t c.
rewrite the current goal using (mul_const_fun_apply c t HcR HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HaltS: a < mul_SNo t c.
rewrite the current goal using HmulEq (from right to left) at position 1.
An exact proof term for the current goal is (RltE_lt a (apply_fun (mul_const_fun c) t) Halt).
We prove the intermediate claim HdivLtS: div_SNo a c < t.
An exact proof term for the current goal is (div_SNo_pos_LtL a c t HaS HcS HtS Hcpos HaltS).
We prove the intermediate claim HdivR: div_SNo a c ∈ R.
An exact proof term for the current goal is (real_div_SNo a HaR c HcR).
We prove the intermediate claim Hray: order_rel R (div_SNo a c) t.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (div_SNo a c) t (RltI (div_SNo a c) t HdivR HtR HdivLtS)).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R (div_SNo a c) x0) t HtR Hray).
Let t be given.
Assume HtRay: t ∈ open_ray_upper R (div_SNo a c).
We will prove t ∈ preimage_of R (mul_const_fun c) (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 (div_SNo a c) x0) t HtRay).
We prove the intermediate claim Hrel: order_rel R (div_SNo a c) t.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R (div_SNo a c) x0) t HtRay).
We prove the intermediate claim HdivLt: Rlt (div_SNo a c) t.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (div_SNo a c) t Hrel).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HdivLtS: div_SNo a c < t.
An exact proof term for the current goal is (RltE_lt (div_SNo a c) t HdivLt).
We prove the intermediate claim HaltS: a < mul_SNo t c.
An exact proof term for the current goal is (div_SNo_pos_LtL' a c t HaS HcS HtS Hcpos HdivLtS).
We prove the intermediate claim HmulR: mul_SNo t c ∈ R.
An exact proof term for the current goal is (real_mul_SNo t HtR c HcR).
We prove the intermediate claim HaltR: Rlt a (mul_SNo t c).
An exact proof term for the current goal is (RltI a (mul_SNo t c) HaR HmulR HaltS).
We prove the intermediate claim Hrel2: order_rel R a (mul_SNo t c).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (mul_SNo t c) HaltR).
We prove the intermediate claim Himg: mul_SNo t c ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepI R (λy0 : set ⇒ order_rel R a y0) (mul_SNo t c) HmulR Hrel2).
We prove the intermediate claim Hpredef: preimage_of R (mul_const_fun c) (open_ray_upper R a) = {x0 ∈ R|apply_fun (mul_const_fun c) x0 ∈ open_ray_upper R a}.
Use reflexivity.
rewrite the current goal using Hpredef (from left to right).
Apply (SepI R (λx0 : set ⇒ apply_fun (mul_const_fun c) x0 ∈ open_ray_upper R a) t HtR) to the current goal.
rewrite the current goal using (mul_const_fun_apply c t HcR HtR) (from left to right).
An exact proof term for the current goal is Himg.
∎