proposition: Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 <= 'Im x) && ~~ (x < 0)).
proof: Proof. apply: (iffP andP) => [[leI0x not_gt0x] | <-]; last first. by rewrite sqrtC_lt0 Im_rootC_ge0. have /eqP := sqrtCK (x ^+ 2); rewrite eqf_sqr => /pred2P[] // defNx. apply: sqrCK; rewrite -real_leNgt ?rpred0 // in not_gt0x; apply/Creal_ImP/le_anti; by rewrite leI0x -oppr_ge0 -raddfN -defNx Im_rootC_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)