proposition: Lemma Str_nth_Qrecip_positives' n : Str_nth n Qrecip_positives = / Str_nth n positives.
proof: Proof. unfold Qrecip_positives. rewrite Str_nth_map. rewrite Qmake_Qdiv. rewrite Str_nth_ppositives'. apply (left_identity (/ Str_nth n positives)). 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