proposition: Lemma sqrtr_eq0 a : (sqrt a == 0) = (a <= 0).
proof: Proof. case: sqrtrP => [/ltW ->|b]; first by rewrite eqxx. case: ltrgt0P => [b_gt0|//|->]; last by rewrite exprS mul0r lexx. by rewrite lt_geF ?pmulr_rgt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)