proposition: Lemma Rabs_derive_1 : forall x:R, 0 < x -> derivable_pt_lim Rabs x 1.
proof: Proof. intros. unfold derivable_pt_lim; intros. exists (mkposreal x H); intros. rewrite (Rabs_right x). - rewrite (Rabs_right (x + h)). + rewrite Rplus_comm. unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r. rewrite Rplus_0_r; unfold Rdiv; rewrite Rinv_r. * rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0. * apply H1. + apply Rle_ge. destruct (Rcase_abs h) as [Hlt|Hgt]. * rewrite (Rabs_left h Hlt) in H2. left; rewrite Rplus_comm; apply Rplus_lt_reg_l with (- h); rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; apply H2. * apply Rplus_le_le_0_compat. -- left; apply H. -- apply Rge_le; apply Hgt. - left; apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia