Let a, b and x be given.
Assume Ha: a ∈ Q_sqrt2_cut.
Assume Hb: b ∈ Q_sqrt2_cut.
Assume HxQ: x ∈ rational_numbers.
Assume Hax: Rlt a x.
Assume Hxb: Rlt x b.
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 prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R a HaQ).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R b HbQ).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R x HxQ).
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 HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
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 Haxlt: a < x.
An exact proof term for the current goal is (RltE_lt a x Hax).
We prove the intermediate claim Hxblt: x < b.
An exact proof term for the current goal is (RltE_lt x b Hxb).
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (mul_SNo x x < 2)) to the current goal.
Assume Hxlt0: x < 0.
We prove the intermediate claim Halt0: a < 0.
An exact proof term for the current goal is (SNoLt_tra a x 0 HaS HxS SNo_0 Haxlt Hxlt0).
We prove the intermediate claim HnegxS: SNo (minus_SNo x).
An exact proof term for the current goal is (SNo_minus_SNo x HxS).
We prove the intermediate claim HnegaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim Hnegxltnega: minus_SNo x < minus_SNo a.
An exact proof term for the current goal is (minus_SNo_Lt_contra a x HaS HxS Haxlt).
We prove the intermediate claim H0ltnegx: 0 < minus_SNo x.
We prove the intermediate claim Hm0: minus_SNo 0 < minus_SNo x.
An exact proof term for the current goal is (minus_SNo_Lt_contra x 0 HxS SNo_0 Hxlt0).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hm0.
We prove the intermediate claim H0ltnega: 0 < minus_SNo a.
We prove the intermediate claim Hm0: minus_SNo 0 < minus_SNo a.
An exact proof term for the current goal is (minus_SNo_Lt_contra a 0 HaS SNo_0 Halt0).
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hm0.
We prove the intermediate claim Hsq: mul_SNo (minus_SNo x) (minus_SNo x) < mul_SNo (minus_SNo a) (minus_SNo a).
An exact proof term for the current goal is (pos_mul_SNo_Lt2 (minus_SNo x) (minus_SNo x) (minus_SNo a) (minus_SNo a) HnegxS HnegxS HnegaS HnegaS H0ltnegx H0ltnegx Hnegxltnega Hnegxltnega).
We prove the intermediate claim Hxxlt: mul_SNo x x < mul_SNo a a.
We will prove mul_SNo x x < mul_SNo a a.
rewrite the current goal using (mul_SNo_minus_minus x x HxS HxS) (from right to left) at position 1.
rewrite the current goal using (mul_SNo_minus_minus a a HaS HaS) (from right to left) at position 1.
An exact proof term for the current goal is Hsq.
We prove the intermediate claim HxxS: SNo (mul_SNo x x).
An exact proof term for the current goal is (SNo_mul_SNo x x HxS HxS).
We prove the intermediate claim HaaS: SNo (mul_SNo a a).
An exact proof term for the current goal is (SNo_mul_SNo a a HaS HaS).
An exact proof term for the current goal is (SNoLt_tra (mul_SNo x x) (mul_SNo a a) 2 HxxS HaaS SNo_2 Hxxlt Haa).
Assume Hxeq0: x = 0.
rewrite the current goal using Hxeq0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL 0 SNo_0) (from left to right).
An exact proof term for the current goal is SNoLt_0_2.
Assume H0ltx: 0 < x.
We prove the intermediate claim H0ltb: 0 < b.
An exact proof term for the current goal is (SNoLt_tra 0 x b SNo_0 HxS HbS H0ltx Hxblt).
We prove the intermediate claim Hsq: mul_SNo x x < mul_SNo b b.
An exact proof term for the current goal is (pos_mul_SNo_Lt2 x x b b HxS HxS HbS HbS H0ltx H0ltx Hxblt Hxblt).
We prove the intermediate claim HxxS: SNo (mul_SNo x x).
An exact proof term for the current goal is (SNo_mul_SNo x x HxS HxS).
We prove the intermediate claim HbbS: SNo (mul_SNo b b).
An exact proof term for the current goal is (SNo_mul_SNo b b HbS HbS).
An exact proof term for the current goal is (SNoLt_tra (mul_SNo x x) (mul_SNo b b) 2 HxxS HbbS SNo_2 Hsq Hbb).
∎