proposition: Lemma derivable_pt_lim_id : forall x:C, derivable_pt_lim id x C1.
proof: Proof. intro; unfold derivable_pt_lim in |- *. intros eps Heps; exists (mkposreal eps Heps); intros h H1 H2; unfold id in |- *; replace ((x + h - x) / h - C1) with C0. rewrite Cnorm_C0 ; assumption. fold C in h. replace (x + h - x) with h by ring. replace (h / h) with C1. unfold Cminus ; rewrite Cadd_opp_r ; reflexivity. unfold Cdiv ; rewrite Cinv_r ; trivial. 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