proposition: Lemma Rseq_pow_fact_little_O : forall r, 0 <= r -> (Rseq_pow r) = o(Rseq_fact).
proof: Proof. assert (HO : forall n, Rseq_pow (INR n) = O(Rseq_fact)). intros n. assert (Hp: 0 <= INR n ^ n). apply pow_le; apply pos_INR. assert (Hf: / INR (fact n) > 0). apply Rinv_0_lt_compat. replace 0 with (INR 0) by reflexivity. apply lt_INR; apply lt_O_fact. exists (INR n ^ n / INR (fact n)); split. replace 0 with (0 * 0)%R by field. apply Rmult_ge_compat; try lra; try left; apply Hf. exists n; intros m Hm. induction Hm. rewrite Rabs_right; [|apply Rle_ge; apply Hp]. rewrite Rabs_right; [|apply Rle_ge; apply pos_INR]. right. unfold Rseq_pow; unfold Rseq_fact; field. apply Rgt_not_eq. replace 0 with (INR 0) by reflexivity. apply lt_INR; apply lt_O_fact. simpl; unfold Rseq_fact; rewrite fact_simpl. rewrite mult_INR. repeat rewrite Rabs_mult. set (K := INR n ^ n / INR (fact n)). replace (K * (Rabs (INR (S m)) * Rabs (INR (fact m)))) with (Rabs (INR (S m)) * (K * (Rabs (INR (fact m))))) by field. apply Rmult_le_compat; try apply Rabs_pos. repeat rewrite Rabs_right; try (apply Rle_ge; apply pos_INR). apply le_INR; lia. apply IHHm. intros r Hr. destruct (IZN (up r)) as [d Hd]. destruct (archimed r) as [H _]. apply le_IZR. eapply Rle_trans. simpl; eexact Hr. left; eexact H. apply Rseq_little_O_big_O_trans with (Rseq_pow (INR d)). apply Rseq_pow_little_O; split. assumption. destruct (archimed r) as [H _]. rewrite Hd in H. rewrite <- INR_IZR_INZ in H. exact H. apply HO. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra