Let c and b be given.
Assume HcR: c ∈ R.
Assume Hcpos: 0 < c.
Assume HbR: b ∈ R.
We will prove preimage_of R (div_const_fun c) (open_ray_lower R b) = open_ray_lower R (mul_SNo b c).
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R (div_const_fun c) (open_ray_lower R b).
We will prove t ∈ open_ray_lower R (mul_SNo b c).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun (div_const_fun c) x0 ∈ open_ray_lower R b) t HtPre).
We prove the intermediate claim Himg: apply_fun (div_const_fun c) t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun (div_const_fun c) x0 ∈ open_ray_lower R b) t HtPre).
We prove the intermediate claim Hrel: order_rel R (apply_fun (div_const_fun c) t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun (div_const_fun c) t) Himg).
We prove the intermediate claim Hrlt: Rlt (apply_fun (div_const_fun c) t) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun (div_const_fun c) t) b Hrel).
We prove the intermediate claim HdivEq: apply_fun (div_const_fun c) t = div_SNo t c.
An exact proof term for the current goal is (div_const_fun_apply c t HcR HtR).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HbcR: mul_SNo b c ∈ R.
An exact proof term for the current goal is (real_mul_SNo b HbR c HcR).
We prove the intermediate claim HbcS: SNo (mul_SNo b c).
An exact proof term for the current goal is (real_SNo (mul_SNo b c) HbcR).
We prove the intermediate claim Hdivlt: div_SNo t c < b.
rewrite the current goal using HdivEq (from right to left).
An exact proof term for the current goal is (RltE_lt (apply_fun (div_const_fun c) t) b Hrlt).
We prove the intermediate claim HmulLt: t < mul_SNo b c.
An exact proof term for the current goal is (div_SNo_pos_LtL' t c b HtS HcS HbS Hcpos Hdivlt).
We prove the intermediate claim Hray: order_rel R t (mul_SNo b c).
An exact proof term for the current goal is (Rlt_implies_order_rel_R t (mul_SNo b c) (RltI t (mul_SNo b c) HtR HbcR HmulLt)).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 (mul_SNo b c)) t HtR Hray).
Let t be given.
Assume HtRay: t ∈ open_ray_lower R (mul_SNo b c).
We will prove t ∈ preimage_of R (div_const_fun c) (open_ray_lower R b).
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 (mul_SNo b c)) t HtRay).
We prove the intermediate claim Hrel: order_rel R t (mul_SNo b c).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 (mul_SNo b c)) t HtRay).
We prove the intermediate claim Hrlt: Rlt t (mul_SNo b c).
An exact proof term for the current goal is (order_rel_R_implies_Rlt t (mul_SNo b c) 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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HbcR: mul_SNo b c ∈ R.
An exact proof term for the current goal is (real_mul_SNo b HbR c HcR).
We prove the intermediate claim HbcS: SNo (mul_SNo b c).
An exact proof term for the current goal is (real_SNo (mul_SNo b c) HbcR).
We prove the intermediate claim HmulLt: t < mul_SNo b c.
An exact proof term for the current goal is (RltE_lt t (mul_SNo b c) Hrlt).
We prove the intermediate claim Hdivlt: div_SNo t c < b.
An exact proof term for the current goal is (div_SNo_pos_LtL t c b HtS HcS HbS Hcpos HmulLt).
We prove the intermediate claim Hray: order_rel R (div_SNo t c) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (div_SNo t c) b (RltI (div_SNo t c) b (real_div_SNo t HtR c HcR) HbR Hdivlt)).
We prove the intermediate claim Himg: div_SNo t c ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 b) (div_SNo t c) (real_div_SNo t HtR c HcR) Hray).
We prove the intermediate claim Hpredef: preimage_of R (div_const_fun c) (open_ray_lower R b) = {x0 ∈ R|apply_fun (div_const_fun c) x0 ∈ open_ray_lower R b}.
Use reflexivity.
rewrite the current goal using Hpredef (from left to right).
Apply (SepI R (λx0 : set ⇒ apply_fun (div_const_fun c) x0 ∈ open_ray_lower R b) t HtR) to the current goal.
rewrite the current goal using (div_const_fun_apply c t HcR HtR) (from left to right).
An exact proof term for the current goal is Himg.
∎