proposition: Lemma Qrecip_positives_help_nbz : forall (x: Qpos) (q:positive), (Zpos (Qden (proj1_sig x)) <= Zpos q)%Z -> NearBy 0 (Qpos2QposInf x) (CoqStreams.map (fun x => 1#x) (ppositives_help q)).
proof: Proof. assert (∀ (q n d : positive), (Zpos d <= Zpos q)%Z → NearBy 0 (Qpos2QposInf (n # d)) (CoqStreams.map (λ x : positive, 1 # x) (ppositives_help q))). { cofix Qrecip_positives_help_nbz. intros q n d Hpq. constructor. - simpl. unfold Qball, QAbsSmall, Qminus. rewrite Qplus_0_r. split. discriminate. change (1*Zpos d <= Zpos n*Zpos q)%Z. apply Zmult_le_compat. apply Pos.le_1_l. exact Hpq. discriminate. discriminate. - apply Qrecip_positives_help_nbz. clear Qrecip_positives_help_nbz. rewrite Zpos_succ_morphism. apply (Z.le_trans _ _ _ Hpq). apply Z.le_succ_diag_r. } intros. destruct x as [[n d] xpos]. destruct n as [|n|n]. inversion xpos. 2: inversion xpos. apply H. exact H0. 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