proposition: Lemma sqrteM x y : 0 <= x -> sqrte (x * y) = sqrte x * sqrte y.
proof: Proof. case: x y => [x||] [y||] //= age0. - by rewrite sqrtrM ?EFinM. - move: age0; rewrite le_eqVlt eqe => /predU1P[<-|x0]. by rewrite mul0e sqrte0 sqrtr0 mul0e. by rewrite mulry gtr0_sg ?mul1e// mulry gtr0_sg ?mul1e// sqrtr_gt0. - move: age0; rewrite mule0 mulrNy lee_fin -sgr_ge0. by case: sgrP; rewrite ?mul0e ?sqrte0// ?mul1e// ler0N1. - rewrite !mulyr; case: (sgrP y) => [->||]. + by rewrite sqrtr0 sgr0 mul0e sqrte0. + by rewrite mul1e/= -sqrtr_gt0 -sgr_gt0 -lte_fin => /gt0_muley->. + by move=> y0; rewrite EFinN mulN1e/= ltr0_sqrtr// sgr0 mul0e. - by rewrite mulyy. - by rewrite mulyNy mule0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed