proposition: Lemma Rseq_fact_cv : Rseq_cv_pos_infty Rseq_fact.
proof: Proof. intros M. assert (forall n, (INR n) <= Rseq_fact n). unfold Rseq_fact. intros n; apply le_INR. destruct n. simpl; repeat constructor. rewrite fact_simpl. pattern (S n) at 1; rewrite <- Nat.mul_1_r. apply Nat.mul_le_mono_l. induction n. simpl; constructor. rewrite fact_simpl; pattern 1%nat; rewrite <- Nat.mul_1_r. apply Nat.mul_le_mono; lia. destruct (IZN (up (Rmax 0 (M + 1)))) as [N Hz]. apply le_0_IZR. destruct (archimed (Rmax 0 (M + 1))) as [Hp _]. left; eapply Rle_lt_trans; [apply RmaxLess1|eexact Hp]. exists N; intros n Hn. eapply Rlt_le_trans with (INR n); [|apply H]. eapply Rlt_le_trans with (INR N); [|apply le_INR; assumption]. rewrite INR_IZR_INZ; rewrite <- Hz. destruct (archimed (Rmax 0 (M + 1))) as [Hp _]. eapply Rlt_trans; [|eexact Hp]. eapply Rlt_le_trans with (M + 1)%R; [lra|apply RmaxLess2]. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra