proposition: Lemma Str_nth_ppositives : forall n, Str_nth n ppositives ≡ P_of_succ_nat n.
proof: Proof. intros n. unfold ppositives. apply nat_of_P_inj. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. change (S n) with ((nat_of_P 1) + n)%nat. generalize 1%positive. induction n. intros c. rewrite Nat.add_comm. reflexivity. intros c. unfold Str_nth in *. simpl. rewrite IHn. rewrite nat_of_P_succ_morphism. apply plus_n_Sm. 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