proposition: Lemma uniqueness_step3 : forall f x v l, limit1_in (fun u => (f (x + u) - f x) / u) (fun u => u <> 0 /\ exists h:R, h * u = v) l 0 -> differentiable_pt_lim f x v l.
proof: Proof. unfold limit1_in, derivable_pt_lim, limit_in, C_dist ; simpl ; unfold C_dist ; intros f x v l Hf_lim v_neq eps eps_pos ; destruct (Hf_lim eps eps_pos) as (alpha, [alpha_pos Halpha]) ; clear Hf_lim. assert (alpha'_pos : 0 < alpha / Cnorm v). unfold Rdiv ; apply Rlt_mult_inv_pos ; [| apply Cnorm_pos_lt] ; assumption. exists (mkposreal (alpha / Cnorm v)%R alpha'_pos) ; intros h h_neq Hyp ; apply Halpha ; rewrite Cminus_0_r ; repeat split. apply Cmult_integral_contrapositive_currified ; [apply IRC_neq_0_compat |] ; assumption. exists (/h)%R. rewrite <- Cmult_assoc. replace ((/ h)%R * h) with C1. apply Cmult_1_l. CusingR_f ; assumption. rewrite Cnorm_Cmult ; apply Rlt_le_trans with (alpha / Cnorm v * Cnorm v)%R. apply Rmult_lt_compat_r. apply Cnorm_pos_lt ; assumption. rewrite Cnorm_IRC_Rabs ; apply Hyp. right ; field ; apply Cnorm_no_R0 ; assumption. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def