Let a, b, d and x be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HdR: d ∈ R.
Assume HxR: x ∈ R.
Assume Hrect: (x,minus_SNo x) ∈ Sorgenfrey_plane_special_rectangle a b d.
We will prove x = a.
Set U to be the term halfopen_interval_left a b.
Set V to be the term halfopen_interval_left (minus_SNo a) d.
We prove the intermediate claim HpUV: (x,minus_SNo x) ∈ setprod U V.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Hrect.
We prove the intermediate claim Hp0U: proj0 (x,minus_SNo x) ∈ U.
An exact proof term for the current goal is (proj0_Sigma U (λ_ : set ⇒ V) (x,minus_SNo x) HpUV).
We prove the intermediate claim Hp1V: proj1 (x,minus_SNo x) ∈ V.
An exact proof term for the current goal is (proj1_Sigma U (λ_ : set ⇒ V) (x,minus_SNo x) HpUV).
We prove the intermediate claim Hp0U0: (x,minus_SNo x) 0 ∈ U.
rewrite the current goal using (proj0_ap_0 (x,minus_SNo x)) (from right to left).
An exact proof term for the current goal is Hp0U.
We prove the intermediate claim Hp1V1: (x,minus_SNo x) 1 ∈ V.
rewrite the current goal using (proj1_ap_1 (x,minus_SNo x)) (from right to left).
An exact proof term for the current goal is Hp1V.
We prove the intermediate claim Hx0: (x,minus_SNo x) 0 = x.
rewrite the current goal using (tuple_pair x (minus_SNo x)) (from right to left).
An exact proof term for the current goal is (pair_ap_0 x (minus_SNo x)).
We prove the intermediate claim Hx1: (x,minus_SNo x) 1 = minus_SNo x.
rewrite the current goal using (tuple_pair x (minus_SNo x)) (from right to left).
An exact proof term for the current goal is (pair_ap_1 x (minus_SNo x)).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using Hx0 (from right to left).
An exact proof term for the current goal is Hp0U0.
We prove the intermediate claim HmxV: (minus_SNo x) ∈ V.
rewrite the current goal using Hx1 (from right to left).
An exact proof term for the current goal is Hp1V1.
We prove the intermediate claim HxUprop: ¬ (Rlt x a) ∧ Rlt x b.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t a) ∧ Rlt t b) x HxU).
We prove the intermediate claim Hnlt_xa: ¬ (Rlt x a).
An exact proof term for the current goal is (andEL (¬ (Rlt x a)) (Rlt x b) HxUprop).
We prove the intermediate claim HmxVprop: ¬ (Rlt (minus_SNo x) (minus_SNo a)) ∧ Rlt (minus_SNo x) d.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t (minus_SNo a)) ∧ Rlt t d) (minus_SNo x) HmxV).
We prove the intermediate claim Hnlt_mx_ma: ¬ (Rlt (minus_SNo x) (minus_SNo a)).
An exact proof term for the current goal is (andEL (¬ (Rlt (minus_SNo x) (minus_SNo a))) (Rlt (minus_SNo x) d) HmxVprop).
We prove the intermediate claim Hnlt_ax: ¬ (Rlt a x).
Assume Hltax: Rlt a x.
We will prove False.
We prove the intermediate claim Hltax_lt: a < x.
An exact proof term for the current goal is (RltE_lt a x Hltax).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hmx_lt_ma: (minus_SNo x) < (minus_SNo a).
An exact proof term for the current goal is (minus_SNo_Lt_contra a x HaS HxS Hltax_lt).
We prove the intermediate claim HmxR: (minus_SNo x) ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
We prove the intermediate claim HmaR: (minus_SNo a) ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
We prove the intermediate claim Hlt: Rlt (minus_SNo x) (minus_SNo a).
An exact proof term for the current goal is (RltI (minus_SNo x) (minus_SNo a) HmxR HmaR Hmx_lt_ma).
An exact proof term for the current goal is (Hnlt_mx_ma Hlt).
An exact proof term for the current goal is (Rle_antisym x a (RleI x a HxR HaR Hnlt_ax) (RleI a x HaR HxR Hnlt_xa)).
∎