proposition: Lemma Qrecip_positives_nbz : forall (n : Z) (d : positive) (U : 0 < n # d), NearBy 0 (Qpos2QposInf (exist _ (n # d) U)) (map (λ x : positive, 1 # x) (ppositives_help (Pplus_LazyNat 1 (LazyPred (LazyNat_of_P d))))).
proof: Proof. intros. apply Qrecip_positives_help_nbz. induction d using Pind;[simpl;auto with *|]. autorewrite with UnLazyNat in *. rewrite nat_of_P_succ_morphism; assert (H:=lt_O_nat_of_P d); destruct (nat_of_P d);[exfalso;auto with *|]; simpl in *; replace (Pplus_LazyNat 2 (LazifyNat n0)) with (Pos.succ (Pplus_LazyNat 1 (LazifyNat n0)));[ repeat rewrite Zpos_succ_morphism; auto with * |]; clear -n0; change 2%positive with (Pos.succ 1); generalize 1%positive; induction n0;intros p;[reflexivity|]; simpl in *; rewrite IHn0; reflexivity. 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