proposition: Lemma derivable_pt_lim_D_in : forall f (df:C -> C) (x:C), D_in f df no_cond x <-> derivable_pt_lim f x (df x).
proof: Proof. intros f df x ; split. unfold D_in, limit1_in, limit_in ; simpl ; unfold C_dist ; intros H 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 ; unfold D_x, no_cond ; repeat split. intro Hf ; apply h_neq ; clear -Hf. apply Cadd_eq_reg_l with x ; rewrite Cadd_0_r ; symmetry ; assumption. rewrite <- Hrew ; assumption. intro. unfold derivable_pt_lim in H. unfold D_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; intros. elim (H eps H0); intros alpha H2; exists (pos alpha); split. apply (cond_pos alpha). intros. elim H1; intros; unfold D_x in H3; elim H3; intros; cut (x0 - x <> 0). intro; generalize (H2 (x0 - x) H7 H4); replace (x + (x0 - x)) with x0. intro; assumption. ring. 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