proposition: Lemma Rseq_inv_poly_little_O : forall d1 d2, (d1 < d2)%nat -> (Rseq_inv_poly d2) = o(Rseq_inv_poly d1).
proof: Proof. intros d1 d2 Hd. eapply Rseq_little_O_asymptotic. intros Wn Xn H; eexact H. exists 1%nat. eapply Rseq_little_O_eq_compat with (Un := fun n => / (INR (S n) ^ d2)) (Vn := fun n => (/ INR (S n) ^ d1)). intros n; unfold Rseq_inv_poly. replace (1 + n)%nat with (S n) by lia. rewrite <- pow_inv; auto with real. intros n; unfold Rseq_inv_poly. replace (1 + n)%nat with (S n) by lia. rewrite <- pow_inv; auto with real. apply Rseq_little_O_inv_contravar. intros eps Heps. destruct (Rseq_poly_little_O d1 d2 Hd eps Heps) as [N HN]. exists N; intros n Hn; apply HN; lia. intros n; apply pow_nonzero; auto with real. intros n; apply pow_nonzero; auto with real. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra