proposition: Lemma limit_inv : forall f D l z, limit1_in f D l z -> l <> 0 -> limit1_in (fun x => / f x) D (/ l) z.
proof: Proof. intros f D l z Hf l_neq ; intros eps eps_pos ; elim (Hf ((Cnorm l) / 2)%R). intros delta1 [delta1_pos Hdelta1] ; elim (Hf (eps * (Rsqr (Cnorm l) / 2))%R). intros delta2 [delta2_pos Hdelta2] ; exists (Rmin delta1 delta2) ; split. unfold Rmin ; case (Rle_dec delta1 delta2); intro H ; assumption. intro x ; generalize (Hdelta2 x); clear Hdelta2 ; intro Hdelta2 ; generalize (Hdelta1 x); clear Hdelta1 ; intro Hdelta1 ; simpl in x. intros [Dx xz_bd] ; cut (D x /\ Cnorm (x - z) < delta1). cut (D x /\ Cnorm (x - z) < delta2). intros H2 H1 ; generalize (Hdelta1 H1) ; clear Hdelta1 ; intro Hdelta1 ; generalize (Hdelta2 H2) ; clear Hdelta2 ; intro Hdelta2. simpl in * ; unfold C_dist in * ; generalize (Cnorm_triang_rev_l l (f x)) ; intro H ; rewrite Cnorm_minus_sym in Hdelta1 ; generalize (Rle_lt_trans (Cnorm l - Cnorm (f x)) (Cnorm (l - f x)) (Cnorm l / 2) H Hdelta1) ; intro H'. generalize (Rplus_lt_compat_l (Cnorm (f x) - Cnorm l / 2) (Cnorm l - Cnorm (f x)) (Cnorm l / 2) H'); replace (Cnorm (f x) - Cnorm l / 2 + (Cnorm l - Cnorm (f x)))%R with (Cnorm l / 2)%R by field. unfold Rminus ; rewrite Rplus_assoc ; rewrite Rplus_opp_l ; rewrite Rplus_0_r ; intro H'' ; cut (f x <> 0). intro fx_neq ; replace (/ f x - / l) with ((l - f x) * / (l * f x)). rewrite Cnorm_Cmult; rewrite Cnorm_inv. cut (/ Cnorm (l * f x) < 2 / Rsqr (Cnorm l)). intro H3; rewrite Cnorm_minus_sym in Hdelta2; cut (0 <= / Cnorm (l * f x)). intro H4 ; generalize (Rmult_le_0_lt_compat (Cnorm (l - f x)) (eps * (Rsqr (Cnorm l) / 2)) (/ Cnorm (l * f x)) (2 / Rsqr (Cnorm l)) (Cnorm_pos ((l - f x))) H4 Hdelta2 H3); replace (eps * (Rsqr (Cnorm l) / 2) * (2 / Rsqr (Cnorm l)))%R with eps. trivial. field ; unfold Rsqr. apply Rmult_integral_contrapositive_currified ; apply Cnorm_no_R0 ; assumption. left ; apply Rinv_0_lt_compat ; apply Cnorm_pos_lt ; apply Cmult_integral_contrapositive_currified ; assumption. rewrite Cmult_comm; rewrite Cnorm_Cmult ; rewrite Rinv_mult. unfold Rsqr, Rdiv ; rewrite Rinv_mult ; repeat rewrite <- Rmult_assoc. apply Rmult_lt_compat_r. apply Rinv_0_lt_compat; apply Cnorm_pos_lt; assumption. apply Rmult_lt_reg_l with (Cnorm (f x) * Cnorm l * / 2)%R. repeat apply Rmult_lt_0_compat ; [| | lra] ; apply Cnorm_pos_lt; assumption. rewrite Rmult_comm ; repeat rewrite <- Rmult_assoc ; rewrite Rinv_l. rewrite Rmult_1_l ; repeat rewrite Rmult_assoc ; replace (Cnorm l * (/ 2 * (2 * / Cnorm l)))%R with 1%R. rewrite Rmult_1_r ; assumption. field ; apply Cnorm_no_R0 ; assumption. apply Cnorm_no_R0 ; assumption. apply Cmult_integral_contrapositive_currified ; assumption. field ; split ; assumption. apply Cnorm_gt_not_eq ; apply Rlt_gt ; apply Rle_lt_trans with (Cnorm l / 2)%R ; [assert (Temp := Cnorm_pos l) ; lra | assumption]. split ; [| apply Rlt_le_trans with (Rmin delta1 delta2) ; [| apply Rmin_r]] ; assumption. split ; [| apply Rlt_le_trans with (Rmin delta1 delta2) ; [| apply Rmin_l]] ; assumption. unfold Rdiv ; repeat apply Rmult_lt_0_compat ; intuition (auto with real) ; apply Cnorm_pos_lt ; assumption. unfold Rdiv ; repeat apply Rmult_lt_0_compat ; intuition (auto with real) ; apply Cnorm_pos_lt ; assumption. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions