proposition: Lemma Rseq_inv_poly_pow_lt_1_little_O : forall d r, 0 < r < 1 -> (Rseq_pow r) = o(Rseq_inv_poly d).
proof: Proof. intros d r [Hr1 Hr2]. eapply Rseq_little_O_asymptotic. intros Wn Xn H; eexact H. exists 1%nat. apply Rseq_little_O_eq_compat with (Un := fun n => / ((/ r) ^ (S n))) (Vn := fun n => (/ INR (S n) ^ d)). intros n; unfold Rseq_pow. replace (1 + n)%nat with (S n) by lia. rewrite pow_inv. rewrite Rinv_inv. reflexivity. intros n; unfold Rseq_inv_poly. replace (1 + n)%nat with (S n) by lia. rewrite <- pow_inv. reflexivity. apply Rseq_little_O_inv_contravar. intros eps Heps. destruct (Rseq_poly_pow_gt_1_little_O d (/ r)) with (eps := eps) as [N HN]. rewrite <- Rinv_1. apply Rinv_lt_contravar. rewrite Rmult_1_r; assumption. assumption. assumption. 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