proposition: Lemma cont_deriv : forall (f d:C -> C) (D:C -> Prop) (z:C), D_in f d D z -> continue_in f D z.
proof: Proof. intros f d D z Hf_D eps eps_pos ; unfold continue_in, D_in, limit1_in, limit_in, Cdiv in Hf_D ; simpl. case (Ceq_dec (d z) 0) ; intro dz_0. elim (Hf_D eps eps_pos) ; clear Hf_D ; intros alpha [alpha_pos Hf_D]. pose (delta := Rmin 1 alpha) ; exists delta ; split. apply Rmin_pos ; auto with real. intros x [Hx x_bd] ; simpl in Hf_D ; unfold C_dist in *. destruct (Ceq_dec x z) as [x_eq_z | x_neq_z]. rewrite x_eq_z ; unfold Cminus ; rewrite Cadd_opp_r. rewrite Cnorm_C0 ; assumption. replace (Cnorm (f x - f z)) with ((Cnorm (f x - f z)) * Cnorm (x - z) * / Cnorm (x - z))%R. apply Rlt_le_trans with (eps * Cnorm (x - z))%R. rewrite Rmult_assoc ; rewrite Rmult_comm ; rewrite Rmult_assoc ; rewrite <- Cnorm_inv. rewrite <- Cnorm_Cmult ; rewrite Rmult_comm ; apply Rmult_lt_compat_r. apply Cnorm_pos_lt ; auto with complex. rewrite Cmult_comm ; replace ((f x - f z) * / (x - z)) with ((f x - f z) * / (x - z) - 0) by auto with complex ; rewrite <- dz_0 ; apply Hf_D ; split ; auto with complex. apply Rlt_le_trans with delta ; [assumption | apply Rmin_r]. auto with complex. apply Rle_trans with (eps * delta)%R. apply Rmult_le_compat_l ; auto with real. rewrite <- Rmult_1_r ; apply Rmult_le_compat_l ; [auto with real | apply Rmin_l]. field ; apply Rgt_not_eq ; apply Cnorm_pos_lt ; auto with complex. assert (eps_2_pos : 0 < eps / 2) by lra ; elim (Hf_D (eps / 2)%R eps_2_pos) ; clear Hf_D ; intros alpha [alpha_pos Hf_D]. pose (delta := Rmin (eps / (2 * Cnorm (d z))) (Rmin (1/2) alpha)) ; exists delta ; split ; [apply Rmin_pos |]. unfold Rdiv ; rewrite Rinv_mult ; repeat apply Rmult_lt_0_compat. assumption. lra. apply Rinv_0_lt_compat ; apply Cnorm_pos_lt ; assumption. apply Rmin_pos ; lra. intros x' [[Dx' z_neq_x'] x'_bd] ; simpl ; unfold C_dist. apply Rlt_trans with (Cnorm (x' - z) * eps + Cnorm (x' - z) * Cnorm (d z))%R. apply Rle_lt_trans with (Cnorm (f x' - f z) * (/ Cnorm (x' - z) * Cnorm (x' - z)))%R. right ; field ; apply Rgt_not_eq ; apply Cnorm_pos_lt ; auto with complex. unfold Rdiv ; rewrite <- Rmult_assoc ; rewrite <- Cnorm_inv, <- Cnorm_Cmult. apply Rle_lt_trans with ((Cnorm ((f x' - f z) * / (x' - z)) + (- Cnorm (d z) + Cnorm (d z))) * Cnorm (x' - z))%R. right ; field. repeat rewrite Rmult_plus_distr_r. replace (Cnorm (d z) * Cnorm (x' - z))%R with (Cnorm (x' - z) * Cnorm (d z))%R by (apply Rmult_comm). rewrite <- Rplus_assoc ; apply Rplus_lt_compat_r. apply Rle_lt_trans with (Cnorm ((f x' - f z) / (x' - z) - d z)* Cnorm (x' - z))%R. rewrite <- Rmult_plus_distr_r ; apply Rmult_le_compat_r ; [apply Cnorm_pos | apply Cnorm_triang_rev_l]. rewrite Rmult_comm ; apply Rmult_lt_compat_l. apply Cnorm_pos_lt ; auto with complex. apply Rlt_trans with (eps /2)%R ; [simpl in Hf_D ; apply Hf_D | lra] ; repeat split ; [| | apply Rlt_le_trans with delta ; [| apply Rle_trans with (Rmin (1 / 2) alpha)%R ; apply Rmin_r]] ; assumption. auto with complex. apply Rlt_trans with (eps / 2 + Cnorm (x' - z) * Cnorm (d z))%R. apply Rplus_lt_compat_r. unfold Rdiv ; rewrite Rmult_comm ; apply Rmult_lt_compat_l ; [assumption |]. apply Rlt_le_trans with (Rmin (eps / (2 * Cnorm (d z))) (Rmin (1 / 2) alpha)). unfold C_dist, delta in x'_bd ; apply x'_bd. apply Rle_trans with (Rmin (1/2) alpha) ; [apply Rmin_r | apply Rle_trans with (1/2)%R ; [apply Rmin_l | right ; field]]. apply Rlt_le_trans with (eps / 2 + eps / 2)%R ; [apply Rplus_lt_compat_l | right ; field]. replace (eps / 2)%R with ((eps / (2 * Cnorm (d z))) * Cnorm (d z))%R by (field ; apply Cnorm_no_R0 ; assumption). apply Rmult_lt_compat_r. apply Cnorm_pos_lt ; assumption. apply Rlt_le_trans with (Rmin (eps / (2 * Cnorm (d z))) (Rmin (1 / 2) alpha)). apply x'_bd. apply Rmin_l. Qed.
imports: Ctacfield Cnorm Cprop_base Classical_Prop Classical_Pred_Type Cmet