proposition: Lemma sqrtE x y: y ^+ 2 = x -> {b : bool | y = (-1) ^+ b * sqrt x}.
proof: Proof. move=> Dx; exists (y != sqrt x); apply/eqP; rewrite mulr_sign if_neg. by case: ifPn => //; apply/implyP; rewrite implyNb -eqf_sqr Dx sqrtK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)