Let x be given.
Assume Hx Hxnn.
We prove the intermediate claim Lx2S: SNo (x ^ 2).
An exact proof term for the current goal is SNo_exp_SNo_nat x Hx 2 nat_2.
We prove the intermediate claim Lx2nn: 0 ≤ x ^ 2.
rewrite the current goal using exp_SNo_nat_2 x Hx (from left to right).
An exact proof term for the current goal is SNo_sqr_nonneg x Hx.
We prove the intermediate claim Lsx2S: SNo (sqrt_SNo_nonneg (x ^ 2)).
An exact proof term for the current goal is SNo_sqrt_SNo_nonneg (x ^ 2) ?? ??.
We prove the intermediate claim Lsx2nn: 0 ≤ sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg (x ^ 2) ?? ??.
We prove the intermediate claim Lsx22xx: sqrt_SNo_nonneg (x ^ 2) * sqrt_SNo_nonneg (x ^ 2) = x * x.
rewrite the current goal using exp_SNo_nat_2 x Hx (from right to left).
An exact proof term for the current goal is sqrt_SNo_nonneg_sqr (x ^ 2) ?? ??.
Apply SNoLeE 0 x SNo_0 Hx Hxnn to the current goal.
Assume H1: 0 < x.
We prove the intermediate claim L1: 0 < sqrt_SNo_nonneg (x ^ 2).
Apply SNoLeE 0 (sqrt_SNo_nonneg (x ^ 2)) SNo_0 ?? ?? to the current goal.
Assume H2: 0 < sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is H2.
Assume H2: 0 = sqrt_SNo_nonneg (x ^ 2).
We will prove False.
Apply SNoLt_irref 0 to the current goal.
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from right to left) at position 2.
We will prove 0 < 0 * 0.
rewrite the current goal using H2 (from left to right) at positions 2 and 3.
rewrite the current goal using Lsx22xx (from left to right).
We will prove 0 < x * x.
An exact proof term for the current goal is mul_SNo_pos_pos x x ?? ?? ?? ??.
Apply SNoLt_trichotomy_or_impred (sqrt_SNo_nonneg (x ^ 2)) x Lsx2S Hx to the current goal.
Assume H2: sqrt_SNo_nonneg (x ^ 2) < x.
We will prove False.
Apply SNoLt_irref (x * x) to the current goal.
We will prove x * x < x * x.
rewrite the current goal using Lsx22xx (from right to left) at position 1.
We will prove sqrt_SNo_nonneg (x ^ 2) * sqrt_SNo_nonneg (x ^ 2) < x * x.
An exact proof term for the current goal is pos_mul_SNo_Lt2 (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2)) x x ?? ?? ?? ?? L1 L1 H2 H2.
Assume H2: sqrt_SNo_nonneg (x ^ 2) = x.
An exact proof term for the current goal is H2.
Assume H2: x < sqrt_SNo_nonneg (x ^ 2).
We will prove False.
Apply SNoLt_irref (x * x) to the current goal.
We will prove x * x < x * x.
rewrite the current goal using Lsx22xx (from right to left) at position 2.
We will prove x * x < sqrt_SNo_nonneg (x ^ 2) * sqrt_SNo_nonneg (x ^ 2).
An exact proof term for the current goal is pos_mul_SNo_Lt2 x x (sqrt_SNo_nonneg (x ^ 2)) (sqrt_SNo_nonneg (x ^ 2)) ?? ?? ?? ?? H1 H1 H2 H2.
Assume H1: 0 = x.
rewrite the current goal using exp_SNo_nat_2 x Hx (from left to right).
rewrite the current goal using H1 (from right to left).
We will prove sqrt_SNo_nonneg (0 * 0) = 0.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
We will prove sqrt_SNo_nonneg 0 = 0.
An exact proof term for the current goal is sqrt_SNo_nonneg_0.
∎