Let x be given.

Assume Hx Hxnonneg.

Apply sqrt_SNo_nonneg_prop1 x Hx Hxnonneg to the current goal.

Assume H _.

Apply H to the current goal.

Assume H _.

An exact proof term for the current goal is H.

∎