proposition: Lemma Rseq_poly_cv : forall d, (d > 0)%nat -> Rseq_cv_pos_infty (Rseq_poly d).
proof: Proof. intros d H M. assert (Hm : forall n, Rseq_poly d n >= INR n). unfold Rseq_poly; induction H; intros n. simpl; lra. eapply Rge_trans with (INR n * INR n)%R. rewrite <- tech_pow_Rmult. apply Rmult_ge_compat_l; [apply Rle_ge; apply pos_INR|apply IHle]. destruct n; auto with real. destruct n; auto with real. left; rewrite <- Rmult_1_r. apply Rmult_gt_compat_l. apply lt_0_INR; lia. apply lt_1_INR; lia. destruct (IZN (up (Rmax 0 (M + 1)))) as [N Hz]. apply le_0_IZR. destruct (archimed (Rmax 0 (M + 1))) as [Hp _]. left; eapply Rle_lt_trans; [apply RmaxLess1|eexact Hp]. exists N; intros n Hn. eapply Rlt_le_trans with (INR n); [|apply Rge_le; apply Hm]. eapply Rlt_le_trans with (INR N); [|apply le_INR; assumption]. rewrite INR_IZR_INZ; rewrite <- Hz. destruct (archimed (Rmax 0 (M + 1))) as [Hp _]. eapply Rlt_trans; [|eexact Hp]. eapply Rlt_le_trans with (M + 1)%R; [lra|apply RmaxLess2]. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra