We will prove (eps_ 1,eps_ 1) ∈ ordsq_E.
Set p to be the term (eps_ 1,eps_ 1).
We prove the intermediate claim HpSq: p ∈ ordered_square.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (eps_ 1) (eps_ 1) eps_1_in_unit_interval eps_1_in_unit_interval).
Apply (SepI ordered_square (λp0 : set ⇒ ∃y0 : set, p0 = (eps_ 1,y0) ∧ Rlt 0 y0 ∧ Rlt y0 1) p HpSq) to the current goal.
We use (eps_ 1) to witness the existential quantifier.
We will prove p = (eps_ 1,eps_ 1) ∧ Rlt 0 (eps_ 1) ∧ Rlt (eps_ 1) 1.
Apply andI to the current goal.
We will prove p = (eps_ 1,eps_ 1) ∧ Rlt 0 (eps_ 1).
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is eps_1_pos_R.
An exact proof term for the current goal is eps_1_lt1_R.
∎