proposition: Lemma Rabs_derive_2 : forall x:R, x < 0 -> derivable_pt_lim Rabs x (-1).
proof: Proof. intros. unfold derivable_pt_lim; intros. cut (0 < - x). - intro; exists (mkposreal (- x) H1); intros. rewrite (Rabs_left x). + rewrite (Rabs_left (x + h)). * replace ((-(x + h) - - x) / h - -1) with 0 by now field. rewrite Rabs_R0; apply H0. * destruct (Rcase_abs h) as [Hlt|Hgt]. -- apply Ropp_lt_cancel. rewrite Ropp_0; rewrite Ropp_plus_distr; apply Rplus_lt_0_compat. ++ apply H1. ++ apply Ropp_0_gt_lt_contravar; apply Hlt. -- rewrite (Rabs_right h Hgt) in H3. apply Rplus_lt_reg_l with (- x); rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; apply H3. + apply H. - apply Ropp_0_gt_lt_contravar; apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia