proposition: Lemma Un_pos : forall n, (0 < n)%nat -> 0 < Un n.
proof: Proof. intros n Hn; unfold Un. unfold Rseq_fact. repeat apply Rmult_lt_0_compat; auto with stirling. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis