proposition: Lemma sqrtrV x : 0 <= x -> sqrt (x^-1) = (sqrt x)^-1.
proof: Proof. case: ltrgt0P => // [x_gt0 _|->]; last by rewrite !(invr0, sqrtr0). have sx_neq0 : sqrt x != 0 by rewrite sqrtr_eq0 -ltNge. apply: (mulfI sx_neq0). by rewrite -sqrtrM !(divff, ltW, sqrtr1) // lt0r_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)