proposition: Lemma uniqueness_limite : forall f x l1 l2, derivable_pt_lim f x l1 -> derivable_pt_lim f x l2 -> l1 = l2.
proof: Proof. intros f x l1 l2 Hf_deriv1 Hf_deriv2 ; assert (H1 := uniqueness_step2 _ _ _ Hf_deriv1) ; assert (H2 := uniqueness_step2 _ _ _ Hf_deriv2) ; apply uniqueness_step1 with f x ; 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