Let x be given.

Assume HxR: x ∈ R.

Apply (order_rel_setprod_R_R_intro x 0 x (eps_ 1)) to the current goal.

Apply orIR to the current goal.

An exact proof term for the current goal is (andI (x = x) (Rlt 0 (eps_ 1)) (λP H ⇒ H) eps_1_pos_R).

∎