proposition: Lemma sqrtrV (R : rcfType) (x : R) : 0 <= x -> Num.sqrt (x^-1) = (Num.sqrt x)^-1.
proof: Proof. move=> x_ge0. case: (x =P 0) => [->|/eqP xD0]; first by rewrite invr0 sqrtr0 invr0. rewrite -[LHS]mul1r -(mulVf (_ : Num.sqrt x != 0)); last first. by rewrite sqrtr_eq0 -ltNge; case: ltrgt0P x_ge0 xD0. by rewrite -mulrA -sqrtrM // divff // sqrtr1 mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp