proposition: Lemma Rser_cv_inv_poly : forall d, (2 <= d)%nat -> {l | Rser_abs_cv (Rseq_inv_poly d) l}.
proof: Proof. intros d Hd. unfold Rser_abs_cv. cut ({l | Rser_cv (Rseq_inv_poly d) l}). intros [l Hl]; exists l. eapply Rser_cv_eq_compat; [|apply Hl]; intro i. destruct i; unfold Rseq_abs; symmetry; apply Rabs_right. apply Rle_refl. unfold Rseq_inv_poly. apply Rle_ge; apply pow_le. apply Rlt_le; apply Rinv_0_lt_compat; INR_solve. apply Rser_pos_maj_cv_shift with (fun (i : nat) => (/ (INR (S i) ^ 2))%R). unfold Rseq_inv_poly; intro n; rewrite <- Rinv_pow; [|INR_solve]. split. apply Rlt_le; apply Rinv_0_lt_compat; apply pow_lt; INR_solve. apply Rle_Rinv. unfold pow; INR_solve; simpl mult; apply Nat.lt_0_succ. apply pow_lt; INR_solve. apply Rle_pow; auto; INR_solve. apply Rser_cv_square_inv. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_cv_facts Lra Rtactic