We will prove sqrt2 ∈ R.

An exact proof term for the current goal is (sqrt_SNo_nonneg_real 2 real_2 (SNoLtLe 0 2 SNoLt_0_2)).

∎