Let b and t be given.
Assume HbR: b ∈ R.
Assume HtR: t ∈ R.
We will prove (apply_fun normalize01_fun t ∈ open_ray_lower R b ↔ Rlt (apply_fun normalize01_fun t) b).
Apply iffI to the current goal.
Assume Hray: apply_fun normalize01_fun t ∈ open_ray_lower R b.
We will prove Rlt (apply_fun normalize01_fun t) b.
We prove the intermediate claim Hrel: order_rel R (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun normalize01_fun t) Hray).
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun normalize01_fun t) b Hrel).
Assume Hlt: Rlt (apply_fun normalize01_fun t) b.
We will prove apply_fun normalize01_fun t ∈ open_ray_lower R b.
We prove the intermediate claim HfR: apply_fun normalize01_fun t ∈ R.
An exact proof term for the current goal is (normalize01_fun_value_in_R t HtR).
We prove the intermediate claim Hrel: order_rel R (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun normalize01_fun t) b Hlt).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 b) (apply_fun normalize01_fun t) HfR Hrel).
∎