proposition: Lemma Rseq_poly_little_O : forall d1 d2, (d1 < d2)%nat -> (Rseq_poly d1) = o(Rseq_poly d2).
proof: Proof. intros d1 d2 Hd. intros eps Heps. unfold Rseq_poly. pose (k := (d2 - d1)%nat). assert (Hk : (k > 0)%nat); [unfold k; lia|]. assert (HM : exists N, forall n, (n >= N)%nat -> /eps < Rseq_poly k n). apply Rseq_poly_cv; assumption. destruct HM as [N HN]. exists N; intros n Hn. replace d2 with (d1 + k)%nat by (unfold k; lia). rewrite pow_add; rewrite Rabs_mult. rewrite Rmult_comm. rewrite Rmult_assoc. pattern (Rabs (INR n ^ d1)) at 1; rewrite <- Rmult_1_r. apply Rmult_le_compat_l; [apply Rabs_pos|]. rewrite <- (Rinv_l eps); [|apply Rgt_not_eq; assumption]. apply Rmult_le_compat_r; [lra|]. rewrite Rabs_right; [|apply Rle_ge; apply pow_le; apply pos_INR]. left; apply HN; assumption. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra