proposition: Lemma sqrt_div_alt : forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y.
proof: Proof. intros x y Hy. unfold sqrt at 2. destruct (Rcase_abs x) as [Hx|Hx]. - unfold Rdiv. rewrite Rmult_0_l. unfold sqrt. destruct (Rcase_abs (x * / y)) as [Hxy|Hxy]. + apply eq_refl. + elim Rge_not_lt with (1 := Hxy). apply Rmult_lt_reg_r with y. * exact Hy. * rewrite Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_0_l. -- exact Hx. -- now apply Rgt_not_eq. - set (Hx' := Rge_le x 0 Hx). clearbody Hx'. clear Hx. apply Rsqr_inj. + apply sqrt_pos. + apply Rle_mult_inv_pos. * apply Rsqrt_positivity. * now apply sqrt_lt_R0. + rewrite Rsqr_div', 2!Rsqr_sqrt. * unfold Rsqr. now rewrite Rsqrt_Rsqrt. * now apply Rlt_le. * now apply Rle_mult_inv_pos. Qed.
imports: Rbase Rfunctions Rsqrt_def