proposition: Lemma Rseq_cv_inv_compat : forall Un lu, Rseq_cv Un lu -> lu <> 0 -> Rseq_cv (/ Un) (/ lu).
proof: Proof. intros Un lu Hu H eps Heps. destruct (Hu (Rabs lu / 2))%R as [Ninf Hinf]. apply Rmult_lt_0_compat; [apply Rabs_pos_lt|lra]; assumption. destruct (Hu (/2 * Rabs lu * Rabs lu * eps))%R as [N HN]. repeat apply Rmult_lt_0_compat; (apply Rabs_pos_lt || lra); assumption. exists (Nat.max Ninf N). intros n Hn. unfold R_dist; unfold Rseq_inv. assert (Habs : Rabs lu / 2 <= Rabs (Un n)). replace (Rabs lu / 2)%R with (Rabs lu - Rabs lu / 2)%R by field. assert (Hr : Rabs (Un n - lu) < Rabs lu / 2). apply Hinf; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. unfold Rabs; repeat destruct Rcase_abs; unfold Rabs in Hr; repeat destruct Rcase_abs in Hr; lra. assert (Hpos : Un n <> 0). unfold Rabs in Habs; repeat destruct Rcase_abs in Habs; try (apply Rlt_not_eq || apply Rgt_not_eq; lra). apply Rgt_not_eq; eapply Rlt_le_trans; [|eexact Habs]. unfold Rdiv; rewrite Ropp_mult_distr_l_reverse; lra. apply Rgt_not_eq; eapply Rlt_le_trans; [|eexact Habs]. unfold Rdiv; apply Rmult_lt_0_compat; auto with real. destruct (Rle_lt_or_eq_dec 0 lu); auto with real. subst; elim H; reflexivity. replace (/ Un n - / lu)%R with (/ lu * / Un n * (lu - Un n))%R by (field; tauto). repeat rewrite Rabs_mult. repeat rewrite Rabs_inv; try assumption. rewrite Rabs_minus_sym. eapply Rlt_le_trans. apply Rmult_lt_compat_l. apply Rmult_lt_0_compat; apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. apply HN; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. replace (/ Rabs lu * / Rabs (Un n) * (/2 * Rabs lu * Rabs lu * eps))%R with (/ Rabs (Un n) * (/2 * Rabs lu) * eps)%R by (field; split; apply Rabs_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 Rabs_pos. destruct Habs as [Habs|Habs]. left; apply Rinv_lt_contravar; [|eassumption]. repeat apply Rmult_lt_0_compat; auto with real; apply Rabs_pos_lt; assumption. rewrite Habs; right; reflexivity. right; field. apply Rabs_no_R0; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra