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