proposition: Lemma differentiable_pt_lim_proj1_1 (f : R -> R) (x y l : R) : differentiable_pt_lim (fun u v => f u) x y l 0 -> derivable_pt_lim f x l.
proof: Proof. intros Df. apply is_derive_Reals ; split => [ | z Hz eps]. by apply @is_linear_scal_l. rewrite -(is_filter_lim_locally_unique _ _ Hz) => {z Hz}. elim (Df eps) ; clear Df ; intros delta Df. exists delta ; simpl in Df ; simpl ; intros. rewrite /minus /plus /opp /scal /= /mult /=. replace (f y0 + - f x + - ((y0 + - x) * l)) with (f y0 - f x - (l * (y0 - x) + 0 * (y - y))) by ring. assert (Rabs (y0 - x) = Rmax (Rabs (y0 - x)) (Rabs (y-y))). rewrite Rmax_comm ; apply sym_equal, Rmax_right. rewrite Rminus_eq_0 Rabs_R0 ; apply Rabs_pos. rewrite /norm /= /abs /=. rewrite H0 ; clear H0. apply (Df _ _ H). rewrite Rminus_eq_0 Rabs_R0 ; apply delta. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive