proposition: Lemma Qn_S : forall d n, (0 < n)%nat -> Qn d n = (/ INR n) ^ d.
proof: Proof. intros d n H; unfold Qn. destruct n; [apply False_ind; lia|reflexivity]. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis