Let z be given.

Assume Hz.

We will prove 0 ≤ sqrt_SNo_nonneg (abs_sqr_CSNo z).

Apply sqrt_SNo_nonneg_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.

∎