proposition: Lemma sqrtrM a b : 0 <= a -> sqrt (a * b) = sqrt a * sqrt b.
proof: Proof. case: (sqrtrP a) => // {}a a_ge0 _; case: (sqrtrP b) => [b_lt0 | {}b b_ge0]. by rewrite mulr0 ler0_sqrtr // nmulr_lle0 ?mulr_ge0. by rewrite mulrACA sqrtr_sqr ger0_norm ?mulr_ge0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)