proposition: Lemma Rseq_poly_fact_little_O : forall d, Rseq_poly d = o(Rseq_fact).
proof: Proof. intros d. eapply Rseq_little_O_trans. apply Rseq_poly_pow_gt_1_little_O. instantiate (1 := 2); lra. apply Rseq_pow_fact_little_O; lra. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra