proposition: Lemma derivable_pt_lim_ln : forall x:R, 0 < x -> derivable_pt_lim ln x (/ x).
proof: Proof. intros; assert (H0 := Dln x H); unfold D_in in H0; unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; unfold Rdist in H0; unfold derivable_pt_lim; intros; elim (H0 _ H1); intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2)); assert (H4 : 0 < alp). { unfold alp; unfold Rmin; case (Rle_dec x0 (x / 2)); intro;unfold Rdiv;lra. } exists (mkposreal _ H4); intros; pattern h at 2; replace h with (x + h - x); [ idtac | ring ]. apply H3; split. 2:{ replace (x + h - x) with h by ring. apply Rlt_le_trans with alp; [ apply H6 | unfold alp; apply Rmin_l ]. } unfold D_x; split. 2:lra. pose proof (Rmin_r _ _ : alp <= _) as H7. unfold Rdiv in H7. unfold Rabs in H6. simpl in H6. destruct (Rcase_abs h) as [Hlt|Hgt];lra. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra