proposition: Lemma Rseq_pow_little_O : forall r1 r2, (0 <= r1 < r2) -> (Rseq_pow r1) = o(Rseq_pow r2).
proof: Proof. intros r1 r2 [Hp Hr] eps Heps. pose (k := (r1 / r2)%R). assert (Hkl : 0 <= k). unfold k; unfold Rdiv; replace 0 with (0 * 0)%R by field. apply Rmult_le_compat; try apply Rle_refl; try lra. left; apply Rinv_0_lt_compat; eapply Rle_lt_trans; eassumption. assert (Hkr : k < 1). unfold k; unfold Rdiv. rewrite <- (Rinv_r r2). apply Rmult_lt_compat_r; [|assumption]. apply Rinv_0_lt_compat; eapply Rle_lt_trans; [eexact Hp|eexact Hr]. apply Rgt_not_eq; eapply Rle_lt_trans; [eexact Hp|eexact Hr]. unfold Rseq_pow. assert (Hk : exists N, forall n, (n >= N)%nat -> Rabs (k ^ n) < eps). apply pow_lt_1_zero; [rewrite Rabs_right|]; try apply Rle_ge; assumption. destruct Hk as [N HN]. exists N; intros n Hn. replace r1 with (k * r2)%R. assert ((k * r2) ^ n = k ^ n * r2 ^ n)%R as ->; swap 1 2. rewrite Rabs_mult. apply Rmult_le_compat_r; [apply Rabs_pos|]. left; apply HN; apply Hn. clear Hn HN; induction n; simpl; try rewrite IHn; field. unfold k; field; apply Rgt_not_eq; eapply Rle_lt_trans; [eexact Hp|eexact Hr]. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra