proposition: Lemma derivable_pt_lim_sqrt : forall x:R, 0 < x -> derivable_pt_lim sqrt x (/ (2 * sqrt x)).
proof: Proof. intros; set (g := fun h:R => sqrt x + sqrt (x + h)). assert (continuity_pt g 0). { replace g with (fct_cte (sqrt x) + comp sqrt (fct_cte x + id))%F; [ idtac | reflexivity ]. apply continuity_pt_plus. - apply continuity_pt_const; unfold constant, fct_cte; intro; reflexivity. - apply continuity_pt_comp. + apply continuity_pt_plus. * apply continuity_pt_const; unfold constant, fct_cte; intro; reflexivity. * apply derivable_continuous_pt; apply derivable_pt_id. + apply sqrt_continuity_pt. unfold plus_fct, fct_cte, id; rewrite Rplus_0_r; apply H. } assert (g 0 <> 0). { unfold g; rewrite Rplus_0_r. assert (0 < sqrt x + sqrt x);[|lra]. apply Rplus_lt_0_compat; apply sqrt_lt_R0; apply H. } intro; assert (H2 := continuity_pt_inv g 0 H0 H1). unfold derivable_pt_lim; intros; unfold continuity_pt in H2; unfold continue_in in H2; unfold limit1_in in H2; unfold limit_in in H2; simpl in H2; unfold Rdist in H2. elim (H2 eps H3); intros alpha H4. elim H4; intros. set (alpha1 := Rmin alpha x). assert (0 < alpha1). { unfold alpha1; unfold Rmin; case (Rle_dec alpha x); intro;lra. } exists (mkposreal alpha1 H7); intros. replace ((sqrt (x + h) - sqrt x) / h) with (/ (sqrt x + sqrt (x + h))). { unfold inv_fct, g in H6; replace (2 * sqrt x) with (sqrt x + sqrt (x + 0)). - apply H6. split. + unfold D_x, no_cond. split. * trivial. * apply (not_eq_sym (A:=R)); exact H8. + unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rlt_le_trans with alpha1. * exact H9. * unfold alpha1; apply Rmin_l. - rewrite Rplus_0_r; ring. } assert (0 <= x + h). { destruct (Rcase_abs h) as [Hlt|Hgt]. 2:lra. rewrite (Rabs_left h Hlt) in H9. apply Rplus_le_reg_l with (- h). rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; left; apply Rlt_le_trans with alpha1. - apply H9. - unfold alpha1; apply Rmin_r. } assert (0 < sqrt x + sqrt (x + h)). { apply Rplus_lt_le_0_compat. - apply sqrt_lt_R0; apply H. - apply sqrt_positivity; apply H10. } apply Rmult_eq_reg_l with (sqrt x + sqrt (x + h)). 2:lra. rewrite Rinv_r. 2:lra. rewrite Rplus_comm; unfold Rdiv; rewrite <- Rmult_assoc; rewrite Rsqr_plus_minus; repeat rewrite Rsqr_sqrt. 2,3: lra. rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; rewrite Rinv_r;lra. Qed.
imports: Rbase Rfunctions Ranalysis1 R_sqrt Lra