We will prove convex_in rational_numbers Q_sqrt2_cut.
We will prove Q_sqrt2_cut ⊆ rational_numbers ∧ ∀a b : set, a ∈ Q_sqrt2_cut → b ∈ Q_sqrt2_cut → order_interval rational_numbers a b ⊆ Q_sqrt2_cut.
Apply andI to the current goal.
An exact proof term for the current goal is Q_sqrt2_cut_sub_Q.
Let a and b be given.
Assume Ha: a ∈ Q_sqrt2_cut.
Assume Hb: b ∈ Q_sqrt2_cut.
We prove the intermediate claim HaQ: a ∈ rational_numbers.
An exact proof term for the current goal is (SepE1 rational_numbers (λq : set ⇒ mul_SNo q q < 2) a Ha).
We prove the intermediate claim HbQ: b ∈ rational_numbers.
An exact proof term for the current goal is (SepE1 rational_numbers (λq : set ⇒ mul_SNo q q < 2) b Hb).
We prove the intermediate claim Haa: mul_SNo a a < 2.
An exact proof term for the current goal is (SepE2 rational_numbers (λq : set ⇒ mul_SNo q q < 2) a Ha).
We prove the intermediate claim Hbb: mul_SNo b b < 2.
An exact proof term for the current goal is (SepE2 rational_numbers (λq : set ⇒ mul_SNo q q < 2) b Hb).
We will prove order_interval rational_numbers a b ⊆ Q_sqrt2_cut.
Let x be given.
Assume Hx: x ∈ order_interval rational_numbers a b.
We will prove x ∈ Q_sqrt2_cut.
We prove the intermediate claim HxQ: x ∈ rational_numbers.
An exact proof term for the current goal is (SepE1 rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ order_rel rational_numbers x0 b) x Hx).
We prove the intermediate claim HxRel: order_rel rational_numbers a x ∧ order_rel rational_numbers x b.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ order_rel rational_numbers x0 b) x Hx).
We prove the intermediate claim Hax: order_rel rational_numbers a x.
An exact proof term for the current goal is (andEL (order_rel rational_numbers a x) (order_rel rational_numbers x b) HxRel).
We prove the intermediate claim Hxb: order_rel rational_numbers x b.
An exact proof term for the current goal is (andER (order_rel rational_numbers a x) (order_rel rational_numbers x b) HxRel).
We prove the intermediate claim Haxlt: Rlt a x.
An exact proof term for the current goal is (order_rel_Q_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_Q_implies_Rlt x b Hxb).
We prove the intermediate claim Hxx: mul_SNo x x < 2.
An exact proof term for the current goal is (Q_sqrt2_cut_between_square a b x Ha Hb HxQ Haxlt Hxblt).
An exact proof term for the current goal is (SepI rational_numbers (λq : set ⇒ mul_SNo q q < 2) x HxQ Hxx).
∎