proposition: Lemma Str_nth_Qrecip_factorials : forall n, (Str_nth n Qrecip_factorials) = 1#(P_of_succ_nat (pred (fact n))).
proof: Proof. intros n. unfold Qrecip_factorials. rewrite Str_nth_map. rewrite <- Str_nth_pfactorials. unfold equiv, stdlib_rationals.Q_eq, Qeq. simpl. apply f_equal. transitivity (Pos.of_nat (Pos.to_nat (Str_nth n pfactorials))). 2: apply Pos2Nat.id. destruct (Pos.to_nat (Str_nth n pfactorials)) eqn:des. 2: apply Pos.of_nat_succ. exfalso. pose proof (Pos2Nat.is_pos (Str_nth n pfactorials)). rewrite des in H. inversion H. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.metric2.Limit Coq.QArith.Qabs Coq.Arith.Arith Coq.QArith.Qpower CoRN.reals.fast.LazyNat Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.theory.series MathClasses.interfaces.abstract_algebra MathClasses.theory.streams