proposition: Lemma differentiable_pt_lim_proj1_0 (f : R -> R) (x y l : R) : derivable_pt_lim f x l -> differentiable_pt_lim (fun u v => f u) x y l 0.
proof: Proof. intros Df eps. apply is_derive_Reals in Df ; elim (proj2 Df x (fun P H => H) eps) ; clear Df ; intros delta Df. exists delta ; simpl ; intros. rewrite Rmult_0_l Rplus_0_r. apply (Rle_trans _ (eps * Rabs (u - x))). rewrite Rmult_comm ; apply (Df _ H). apply Rmult_le_compat_l. apply Rlt_le, eps. apply RmaxLess1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive