proposition: Lemma Qrecip_factorial_bounded : StreamBounds Qrecip_positives (CoqStreams.tl Qrecip_factorials).
proof: Proof. unfold Qrecip_positives, Qrecip_factorials, ppositives, pfactorials. cut (forall (p q:positive), StreamBounds (CoqStreams.map (fun x : positive => 1 # x) (ppositives_help p)) (CoqStreams.tl (CoqStreams.map (fun x : positive => 1 # x) (pfactorials_help p q)))). intros H. apply (H 1%positive 1%positive). auto with *. cofix Qrecip_factorial_bounded. constructor. simpl. split. discriminate. change (Zpos p <= Zpos p * Zpos q)%Z. rewrite Z.mul_comm. apply (Z.mul_le_mono_nonneg_r 1 (Zpos q) (Zpos p)). discriminate. apply Pos.le_1_l. simpl in *. apply Qrecip_factorial_bounded. 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