Let a be given.
Assume HaR.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ R ∖ {a,a}.
We will prove x ∈ {x0 ∈ R|Rlt x0 a} ∪ {x0 ∈ R|Rlt a x0}.
We prove the intermediate claim Hxpair: x ∈ R ∧ x ∉ {a,a}.
An exact proof term for the current goal is (setminusE R {a,a} x Hx).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (andEL (x ∈ R) (x ∉ {a,a}) Hxpair).
We prove the intermediate claim HxNot: x ∉ {a,a}.
An exact proof term for the current goal is (andER (x ∈ R) (x ∉ {a,a}) Hxpair).
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 HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
Apply (SNoLt_trichotomy_or_impred x a HxS HaS (x ∈ {x0 ∈ R|Rlt x0 a} ∪ {x0 ∈ R|Rlt a x0})) to the current goal.
Assume Hxlt: x < a.
We prove the intermediate claim HxRlt: Rlt x a.
An exact proof term for the current goal is (RltI x a HxR HaR Hxlt).
We prove the intermediate claim HxLeft: x ∈ {x0 ∈ R|Rlt x0 a}.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt x0 a) x HxR HxRlt).
An exact proof term for the current goal is (binunionI1 {x0 ∈ R|Rlt x0 a} {x0 ∈ R|Rlt a x0} x HxLeft).
Assume Hxeq: x = a.
We prove the intermediate claim Hxinpair: x ∈ {a,a}.
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is (UPairI1 a a).
We prove the intermediate claim Hfalse: False.
An exact proof term for the current goal is (HxNot Hxinpair).
An exact proof term for the current goal is (FalseE Hfalse (x ∈ {x0 ∈ R|Rlt x0 a} ∪ {x0 ∈ R|Rlt a x0})).
Assume Halt: a < x.
We prove the intermediate claim HxRlt: Rlt a x.
An exact proof term for the current goal is (RltI a x HaR HxR Halt).
We prove the intermediate claim HxRight: x ∈ {x0 ∈ R|Rlt a x0}.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a x0) x HxR HxRlt).
An exact proof term for the current goal is (binunionI2 {x0 ∈ R|Rlt x0 a} {x0 ∈ R|Rlt a x0} x HxRight).
Let x be given.
Assume Hx: x ∈ {x0 ∈ R|Rlt x0 a} ∪ {x0 ∈ R|Rlt a x0}.
We will prove x ∈ R ∖ {a,a}.
Apply (binunionE {x0 ∈ R|Rlt x0 a} {x0 ∈ R|Rlt a x0} x Hx) to the current goal.
Assume HxLeft: x ∈ {x0 ∈ R|Rlt x0 a}.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt x0 a) x HxLeft).
We prove the intermediate claim HxRlt: Rlt x a.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt x0 a) x HxLeft).
We prove the intermediate claim HxNot: x ∉ {a,a}.
Assume Hxin: x ∈ {a,a}.
We prove the intermediate claim Hxeq: x = a.
Apply (UPairE x a a Hxin (x = a)) to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1.
An exact proof term for the current goal is H1.
We prove the intermediate claim Haa: Rlt a a.
rewrite the current goal using Hxeq (from right to left) at position 1.
An exact proof term for the current goal is HxRlt.
An exact proof term for the current goal is ((not_Rlt_refl a HaR) Haa).
An exact proof term for the current goal is (setminusI R {a,a} x HxR HxNot).
Assume HxRight: x ∈ {x0 ∈ R|Rlt a x0}.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0) x HxRight).
We prove the intermediate claim HxRlt: Rlt a x.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0) x HxRight).
We prove the intermediate claim HxNot: x ∉ {a,a}.
Assume Hxin: x ∈ {a,a}.
We prove the intermediate claim Hxeq: x = a.
Apply (UPairE x a a Hxin (x = a)) to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1.
An exact proof term for the current goal is H1.
We prove the intermediate claim Haa: Rlt a a.
rewrite the current goal using Hxeq (from right to left) at position 2.
An exact proof term for the current goal is HxRlt.
An exact proof term for the current goal is ((not_Rlt_refl a HaR) Haa).
An exact proof term for the current goal is (setminusI R {a,a} x HxR HxNot).
∎