proposition: Lemma derive_pt_eq : forall f x l (pr:derivable_pt f x), derive_pt f x pr = l <-> derivable_pt_lim f x l.
proof: Proof. intros f x l pr ; split ; intro Hf_deriv. assert (H := proj2_sig pr) ; unfold derive_pt in Hf_deriv ; rewrite Hf_deriv in H ; assumption. assert (H := proj2_sig pr) ; unfold derivable_pt_abs in H ; assert (H' := uniqueness_limite _ _ _ _ Hf_deriv H) ; symmetry ; 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