proposition: Lemma uniqueness_limite : forall f (x l1 l2:R), derivable_pt_lim f x l1 -> derivable_pt_lim f x l2 -> l1 = l2.
proof: Proof. intros. assert (H1 := uniqueness_step2 _ _ _ H). assert (H2 := uniqueness_step2 _ _ _ H0). assert (H3 := uniqueness_step1 _ _ _ _ H1 H2). assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv