We will prove 0 < sqrt2.
We prove the intermediate claim Hs2R: sqrt2 ∈ R.
An exact proof term for the current goal is sqrt2_in_R.
We prove the intermediate claim Hs2S: SNo sqrt2.
An exact proof term for the current goal is (real_SNo sqrt2 Hs2R).
We prove the intermediate claim H0le2: 0 ≤ 2.
An exact proof term for the current goal is (SNoLtLe 0 2 SNoLt_0_2).
We prove the intermediate claim H0les2: 0 ≤ sqrt2.
An exact proof term for the current goal is (sqrt_SNo_nonneg_nonneg 2 SNo_2 H0le2).
Apply (SNoLt_trichotomy_or_impred sqrt2 0 Hs2S SNo_0 (0 < sqrt2)) to the current goal.
Assume Hs2lt0: sqrt2 < 0.
Apply FalseE to the current goal.
We prove the intermediate claim H0lt0: 0 < 0.
An exact proof term for the current goal is (SNoLeLt_tra 0 sqrt2 0 SNo_0 Hs2S SNo_0 H0les2 Hs2lt0).
An exact proof term for the current goal is ((SNoLt_irref 0) H0lt0).
Assume Heq: sqrt2 = 0.
Apply FalseE to the current goal.
We prove the intermediate claim Htmp: mul_SNo sqrt2 sqrt2 = 2.
An exact proof term for the current goal is (sqrt_SNo_nonneg_sqr 2 SNo_2 (SNoLtLe 0 2 SNoLt_0_2)).
We prove the intermediate claim Hs2sqr0: mul_SNo 0 0 = 2.
rewrite the current goal using Heq (from right to left) at position 1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim H00: mul_SNo 0 0 = 0.
An exact proof term for the current goal is (mul_SNo_zeroL 0 SNo_0).
We prove the intermediate claim H02: 0 = 2.
rewrite the current goal using H00 (from right to left) at position 1.
An exact proof term for the current goal is Hs2sqr0.
An exact proof term for the current goal is (neq_0_2 H02).
Assume H0lts2: 0 < sqrt2.
An exact proof term for the current goal is H0lts2.
∎