Let x and y be given.
Assume Hx Hy Hxnn Hxy.
Apply SNoLeE x y Hx Hy Hxy to the current goal.
Assume H1: x < y.
We will prove sqrt_SNo_nonneg x ≤ sqrt_SNo_nonneg y.
Apply SNoLtLe to the current goal.
We will prove sqrt_SNo_nonneg x < sqrt_SNo_nonneg y.
An exact proof term for the current goal is sqrt_SNo_nonneg_mon_strict x y Hx Hy Hxnn H1.
Assume H1: x = y.
rewrite the current goal using H1 (from left to right).
Apply SNoLe_ref to the current goal.
∎