proposition: Lemma uniqueness_limite : forall f (x v l1 l2 : C), v <> 0 -> differentiable_pt_lim f x v l1 -> differentiable_pt_lim f x v l2 -> l1 = l2.
proof: Proof. intros f x v l1 l2 v_neq Hf_deriv1 Hf_deriv2 ; assert (H1 := uniqueness_step2 _ _ _ _ v_neq Hf_deriv1) ; assert (H2 := uniqueness_step2 _ _ _ _ v_neq Hf_deriv2) ; apply uniqueness_step1 with f x v ; assumption. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def