Let x be given.

Assume Hx Hxnonneg.

Apply sqrt_SNo_nonneg_prop1a x Hx Hxnonneg to the current goal.

Let w be given.

Assume Hw Hwnonneg.

Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) w Hw to the current goal.

Assume Hw1 Hw2 Hw3 Hw4.

An exact proof term for the current goal is sqrt_SNo_nonneg_prop1 w Hw3 Hwnonneg.

∎