proposition: Lemma sinStream_pos : ∀ x : positive * (AQ * AQ), 0 < snd (snd x) → 0 < snd (ARsinStream x).
proof: Proof. assert (0 = ZtoAQ 0) as zero_int. { destruct H4. destruct aq_ints_mor, semiringmor_plus_mor. rewrite preserves_mon_unit. reflexivity. } intros. destruct x; simpl. simpl in H5. apply AQmult_lt_0_compat. apply AQmult_lt_0_compat. apply AQmult_lt_0_compat. apply AQmult_lt_0_compat. exact H5. exact dpos. exact dpos. rewrite zero_int. apply (strictly_order_preserving (cast Z AQ)). reflexivity. rewrite zero_int. apply (strictly_order_preserving (cast Z AQ)). reflexivity. Qed.
imports: Coq.QArith.Qround Coq.QArith.Qpower MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.MetricMorphisms CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRsin CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARArith