proposition: Lemma uniqueness_step1 : forall f (x v l1 l2 : C), v <> 0 -> limit1_in (fun u => (f (x + u) - f x) / u) (fun u => u <> 0 /\ exists h:R, h * u = v) l1 0 -> limit1_in (fun u => (f (x + u) - f x) / u) (fun u => u <> 0 /\ exists h:R, h * u = v) l2 0 -> l1 = l2.
proof: Proof. intros f x v l1 l2 v_neq Hl1 Hl2 ; apply (single_limit (fun u => (f (x + u) - f x) / u) (fun u => u <> 0 /\ exists h:R, h * u = v) l1 l2 0); try assumption. intros alp alp_pos. case (Rlt_le_dec (Cnorm v) alp) ; intro alp_bd. exists v ; repeat split. assumption. exists 1%R ; CusingR_f. unfold C_dist ; rewrite Cminus_0_r ; assumption. exists (v * ((alp / 2) / Cnorm v)) ; repeat split. unfold Cdiv ; repeat apply Cmult_integral_contrapositive_currified. assumption. apply IRC_neq_0_compat ; apply Rgt_not_eq ; assumption. apply Cinv_neq_0_compat ; apply IRC_neq_0_compat ; apply Rgt_not_eq ; lra. apply Cinv_neq_0_compat ; apply IRC_neq_0_compat ; apply Cnorm_no_R0 ; assumption. exists (2 * Cnorm v / alp)%R. unfold Rdiv, Cdiv. CusingR_f ; try split. apply Cnorm_no_R0 ; assumption. apply Rgt_not_eq ; assumption. apply Cnorm_no_R0 ; assumption. apply Rgt_not_eq ; assumption. unfold C_dist ; rewrite Cminus_0_r. unfold Cdiv ; rewrite Cmult_comm ; repeat rewrite Cnorm_Cmult. repeat rewrite Cnorm_inv. rewrite Cnorm_invol, Rmult_assoc, Rinv_l. rewrite Rmult_1_r ; rewrite <- Cnorm_inv. rewrite <- Cnorm_Cmult. replace (alp * / 2)%C with (IRC (alp / 2)%R). rewrite Cnorm_IRC_Rabs, Rabs_right. lra. lra. clear ; CusingR_f. apply IRC_neq_0_compat ; apply Rgt_not_eq ; lra. apply Cnorm_no_R0 ; assumption. apply IRC_neq_0_compat ; apply Cnorm_no_R0 ; assumption. apply IRC_neq_0_compat ; apply Rgt_not_eq ; lra. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def