Let x be given.

Assume Hx Hxnonneg.

Apply sqrt_SNo_nonneg_prop1b x Hx Hxnonneg to the current goal.

An exact proof term for the current goal is SNo_sqrtaux_0_1_prop x Hx Hxnonneg.

∎