Let z be given.

Assume Hz.

We will prove SNo (sqrt_SNo_nonneg (abs_sqr_CSNo z)).

Apply SNo_sqrt_SNo_nonneg to the current goal.

An exact proof term for the current goal is SNo_abs_sqr_CSNo z Hz.

An exact proof term for the current goal is abs_sqr_CSNo_nonneg z Hz.

∎