proposition: Lemma derivable_differentiable_pt_abs : forall f x l, derivable_pt_abs f x l -> forall v, differentiable_pt_abs f x v l.
proof: Proof. intros f x l Hl v v_neq eps eps_pos ; destruct (Hl eps eps_pos) as [delta Hdelta] ; assert (delta'_pos : (0 < delta / Cnorm v)%R). apply Rlt_mult_inv_pos ; [apply delta | apply Cnorm_pos_lt ; assumption]. pose (delta' := mkposreal (delta / Cnorm v)%R delta'_pos) ; exists delta' ; intros h h_neq h_ub ; apply Hdelta. apply Cmult_integral_contrapositive_currified ; [apply IRC_neq_0_compat |] ; assumption. rewrite Cnorm_Cmult. apply Rlt_le_trans with (delta' * Cnorm v)%R. apply Rmult_lt_compat_r. apply Cnorm_pos_lt ; assumption. rewrite Cnorm_IRC_Rabs ; assumption. unfold delta', Rdiv ; simpl ; rewrite Rmult_assoc, Rinv_l. right ; field. apply Cnorm_no_R0 ; assumption. Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv