Let x be given.

Assume Hx Hxnonneg.

Let k be given.

Assume Hk.

Apply SNo_sqrtaux_0_1_prop x Hx Hxnonneg k Hk to the current goal.

Assume _ H.

An exact proof term for the current goal is H.

∎