proposition: Lemma derive_pt_D_in : forall (f df:C -> C) (x:C) (pr:derivable_pt f x), D_in f df no_cond x <-> derive_pt f x pr = df x.
proof: Proof. intros f df x pr ; split. unfold D_in, limit1_in, limit_in ; simpl ; unfold C_dist ; intros. apply derive_pt_eq_0. intros eps eps_pos ; destruct (H eps eps_pos) as [alpha [alpha_pos Halpha]] ; exists (mkposreal alpha alpha_pos) ; intros h h_neq h_bd. fold C in h ; assert (Hrew : h = (x + h) - x) by ring ; rewrite Hrew at 2. apply Halpha ; split. unfold D_x, no_cond ; split ; [trivial |]. intro Hf ; apply h_neq ; clear -Hf. apply Cadd_eq_reg_l with x ; rewrite Cadd_0_r ; symmetry ; assumption. rewrite <- Hrew ; assumption. intro H. assert (H0 := derive_pt_eq_1 f x (df x) pr H). intros eps eps_pos. destruct (H0 eps eps_pos) as [alpha Halpha] ; exists alpha ; split. exact (cond_pos alpha). intros a [Ha a_bd] ; unfold D_x in Ha ; destruct Ha as [_ Ha] ; assert (Temp : a - x <> 0) by (auto with complex). generalize (Halpha (a - x) Temp a_bd); replace (x + (a - x)) with a. intro; assumption. auto with complex. 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