proposition: Lemma expStream_pos : ∀ x : positive * (AQ * AQ), 0 < snd (snd x) → 0 < snd (ARexpStream x).
proof: Proof. intros. unfold ARexpStream. simpl. assert (AQtoQ 0 == 0). apply rings.preserves_0. destruct aq_strict_order_embed. apply strict_order_embedding_reflecting. rewrite rings.preserves_mult, rings.preserves_0. apply (Qle_lt_trans _ (AQtoQ (snd (snd x)) * 0)). rewrite Qmult_0_r. apply Qle_refl. apply Qmult_lt_l. rewrite <- H6. apply strict_order_embedding_preserving, H5. pose proof AQtoQ_ZtoAQ. unfold cast in H7. rewrite H7. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program MathClasses.misc.workaround_tactics CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qround Coq.QArith.Qabs CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRexp CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.fast.CRpower CoRN.metric2.MetricMorphisms CoRN.reals.faster.ARAlternatingSum MathClasses.interfaces.abstract_algebra MathClasses.orders.minmax MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.reals.faster.ARArith