Let a and b be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ order_interval R a b.
We will prove x ∈ open_interval a b.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R a x0 ∧ order_rel R x0 b) x Hx).
We prove the intermediate claim Hconj: order_rel R a x ∧ order_rel R x b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0 ∧ order_rel R x0 b) x Hx).
We prove the intermediate claim Hax: order_rel R a x.
An exact proof term for the current goal is (andEL (order_rel R a x) (order_rel R x b) Hconj).
We prove the intermediate claim Hxb: order_rel R x b.
An exact proof term for the current goal is (andER (order_rel R a x) (order_rel R x b) Hconj).
We prove the intermediate claim Haxlt: Rlt a x.
An exact proof term for the current goal is (order_rel_R_implies_Rlt a x Hax).
We prove the intermediate claim Hxblt: Rlt x b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt x b Hxb).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x HxR (andI (Rlt a x) (Rlt x b) Haxlt Hxblt)).
Let x be given.
Assume Hx: x ∈ open_interval a b.
We will prove x ∈ order_interval R a b.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x Hx).
We prove the intermediate claim Hconj: Rlt a x ∧ Rlt x b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x Hx).
We prove the intermediate claim Hax: Rlt a x.
An exact proof term for the current goal is (andEL (Rlt a x) (Rlt x b) Hconj).
We prove the intermediate claim Hxb: Rlt x b.
An exact proof term for the current goal is (andER (Rlt a x) (Rlt x b) Hconj).
We prove the intermediate claim Haxrel: order_rel R a x.
An exact proof term for the current goal is (Rlt_implies_order_rel_R a x Hax).
We prove the intermediate claim Hxbrel: order_rel R x b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R x b Hxb).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R a x0 ∧ order_rel R x0 b) x HxR (andI (order_rel R a x) (order_rel R x b) Haxrel Hxbrel)).
∎