proposition: Lemma uniqueness_step2 : forall f (x : C) (v : C) (l : C), v <> 0 -> differentiable_pt_lim 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.
proof: Proof. unfold derivable_pt_lim, limit1_in, limit_in. intros f x v l v_neq Hf_deriv eps eps_pos ; destruct (Hf_deriv v_neq eps eps_pos) as ([alpha alpha_pos], Halpha) ; clear Hf_deriv ; exists (alpha * Cnorm v)%R ; split. apply Rmult_lt_0_compat ; [| apply Cnorm_pos_lt]; eauto with *. intros h [[h_neq [u h_rew]] Hh] ; simpl in * ; unfold C_dist in *. assert (u_neq : (u <> 0)%R). intro Hf ; apply v_neq ; rewrite <- h_rew, Hf ; CusingR_f. replace h with ((/u)%R * v). apply (Halpha (/u)%R). apply Rinv_neq_0_compat ; assumption. rewrite Cminus_0_r in Hh. replace (Rabs (/u))%R with (Cnorm h / Cnorm v)%R. apply Rlt_le_trans with (alpha * Cnorm v * / Cnorm v)%R. unfold Rdiv ; apply Rmult_lt_compat_r. apply Rinv_0_lt_compat ; apply Cnorm_pos_lt ; assumption. assumption. right ; field ; apply Cnorm_no_R0 ; assumption. rewrite <- h_rew. unfold Rdiv ; rewrite <- Cnorm_inv. rewrite <- Cnorm_Cmult. replace (h * / (u * h)) with (IRC (/ u)). apply Cnorm_IRC_Rabs. rewrite Cinv_mult_distr, Cmult_comm, Cmult_assoc, Cinv_l, Cmult_1_r. clear -u_neq ; CusingR ; field ; assumption. assumption. apply IRC_neq_0_compat ; assumption. assumption. apply Cmult_integral_contrapositive_currified ; [apply IRC_neq_0_compat |] ; assumption. rewrite <- h_rew. replace (IRC (/ u)) with (/ u). field ; apply IRC_neq_0_compat ; assumption. CusingR_f ; assumption. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def