proposition: Lemma uniqueness_step2 : forall f (x l:R), derivable_pt_lim f x l -> limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0.
proof: Proof. unfold derivable_pt_lim; intros; unfold limit1_in; unfold limit_in; intros. assert (H1 := H eps H0). elim H1; intros. exists (pos x0). split. - apply (cond_pos x0). - simpl; unfold Rdist; intros. elim H3; intros. apply H2; [ assumption | unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5; assumption ]. Qed.
imports: Rbase Rfunctions Rlimit Rderiv