proposition: Lemma Cseq_cv_inv_compat : lu <> 0 -> Cseq_cv (/ Un) (/ lu).
proof: Proof. intros H eps Heps. destruct (Hu (Cnorm lu / 2))%R as [Ninf Hinf]. apply Rmult_lt_0_compat; [apply Cnorm_pos_lt|lra]; assumption. destruct (Hu (/2 * Cnorm lu * Cnorm lu * eps))%R as [N HN]. repeat apply Rmult_lt_0_compat; (apply Cnorm_pos_lt || lra); assumption. exists (Nat.max Ninf N). intros n Hn. unfold R_dist; unfold Cseq_inv. assert (Habs : Cnorm lu / 2 <= Cnorm (Un n)). replace (Cnorm lu / 2)%R with (Cnorm lu - Cnorm lu / 2)%R by field. assert (Hr : Cnorm (Un n - lu) < Cnorm lu / 2). apply Hinf; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite Cnorm_minus_sym in Hr. assert (Temp := Cnorm_triang_rev_r (lu - Un n) lu). replace (Cnorm (Un n)) with (Cnorm (- Un n)) by (apply Cnorm_opp) ; replace (- Un n)%C with (lu - Un n - lu)%C by field. lra. assert (Hpos : Un n <> 0). case (Ceq_or_neq_C0 (Un n)) ; intro HUn. apply False_ind ; elim (Rlt_irrefl 0). apply Rlt_le_trans with (Cnorm lu / 2)%R. unfold Rdiv ; rewrite Rmult_comm ; replace (/2)%R with (Rabs (/2)) by (apply Rabs_right ; lra) ; rewrite <- Cnorm_mult ; apply Cnorm_pos_lt ; apply Cnorm_gt_not_eq ; rewrite Cnorm_mult ; apply Rmult_lt_0_compat. rewrite Rabs_right ; lra. apply Cnorm_pos_lt ; assumption. Set Printing All. apply Rle_trans with (Cnorm (Un n)) ; [assumption | rewrite HUn ; rewrite Cnorm_C0 ; right ; trivial]. assumption. replace (/ Un n - / lu)%C with (/ lu * / Un n * (lu - Un n))%C by (field; tauto). repeat (rewrite Cnorm_Cmult). repeat rewrite Cnorm_inv; try assumption. rewrite Cnorm_minus_sym. eapply Rlt_le_trans. apply Rmult_lt_compat_l. apply Rmult_lt_0_compat; apply Rinv_0_lt_compat; apply Cnorm_pos_lt; assumption. apply HN; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. replace (/ Cnorm lu * / Cnorm (Un n) * (/2 * Cnorm lu * Cnorm lu * eps))%R with (/ Cnorm (Un n) * (/2 * Cnorm lu) * eps)%R by (field; split ; apply Cnorm_no_R0 ; assumption). rewrite <- Rmult_1_l. apply Rmult_le_compat_r; auto with real. eapply Rle_trans. apply Rmult_le_compat_r. replace 0%R with (0 * 0)%R by field. apply Rmult_le_compat; auto with real; apply Cnorm_pos. destruct Habs as [Habs|Habs]. left; apply Rinv_lt_contravar; [|eassumption]. repeat apply Rmult_lt_0_compat; auto with real; apply Cnorm_pos_lt; assumption. rewrite Habs; right; reflexivity. right; field. apply Cnorm_no_R0; assumption. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def