proposition: Lemma Str_nth_ppositives' n : inject_Z (Zpos (Str_nth n ppositives)) = Str_nth n positives.
proof: Proof. rewrite Str_nth_ppositives, Str_nth_positives. rewrite Z.P_of_succ_nat_Zplus. rewrite <-(naturals.to_semiring_unique (Basics.compose inject_Z Z_of_nat)). unfold Basics.compose. rewrite <-(rings.preserves_1 (f:=inject_Z)). rewrite <-rings.preserves_plus. now rewrite commutativity. 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