proposition: Lemma derive_pt_eq_0 : forall f x l (pr:derivable_pt f x), derivable_pt_lim f x l -> derive_pt f x pr = l.
proof: Proof. intros f x l pr ; destruct (derive_pt_eq f x l pr) ; 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