proposition: Lemma sqrt_inv x : sqrt (/ x) = / sqrt x.
proof: Proof. destruct (Rlt_or_le 0 x) as [H|H]. - assert (sqrt x <> 0). + apply Rgt_not_eq. now apply sqrt_lt_R0. + apply Rmult_eq_reg_r with (sqrt x); auto. rewrite Rinv_l; auto. rewrite <- sqrt_mult_alt. * now rewrite -> Rinv_l, sqrt_1; auto with real. * apply Rlt_le. now apply Rinv_0_lt_compat. - rewrite sqrt_neg_0 with (1 := H). rewrite sqrt_neg_0. + apply eq_sym, Rinv_0. + destruct H as [H| ->]. * now apply Rlt_le, Rinv_lt_0_compat. * rewrite Rinv_0. apply Rle_refl. Qed.
imports: Rbase Rfunctions Rsqrt_def