proposition: Lemma sqrt_mult_alt : forall x y : R, 0 <= x -> sqrt (x * y) = sqrt x * sqrt y.
proof: Proof. intros x y Hx. unfold sqrt at 3. destruct (Rcase_abs y) as [Hy|Hy]. - rewrite Rmult_0_r. destruct Hx as [Hx'|Hx']. + unfold sqrt. destruct (Rcase_abs (x * y)) as [Hxy|Hxy]. * apply eq_refl. * elim Rge_not_lt with (1 := Hxy). rewrite <- (Rmult_0_r x). now apply Rmult_lt_compat_l. + rewrite <- Hx', Rmult_0_l. exact sqrt_0. - apply Rsqr_inj. + apply sqrt_pos. + apply Rmult_le_pos. * apply sqrt_pos. * apply Rsqrt_positivity. + rewrite Rsqr_mult, 2!Rsqr_sqrt. * unfold Rsqr. now rewrite Rsqrt_Rsqrt. * exact Hx. * apply Rmult_le_pos. -- exact Hx. -- now apply Rge_le. Qed.
imports: Rbase Rfunctions Rsqrt_def