proposition: Lemma derivable_pt_id : forall x:C, derivable_pt id x.
proof: Proof. unfold derivable_pt in |- *; intro. exists 1. apply derivable_pt_lim_id. 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