proposition: Lemma AQmult_lt_0_compat : forall a b : AQ, 0 < a -> 0 < b -> 0 < a*b.
proof: Proof. intros. apply (strictly_order_reflecting (cast AQ Q)). pose proof (rings.preserves_0 (f:=cast AQ Q)). rewrite H7. rewrite rings.preserves_mult. rewrite <- (Qmult_0_l ('b)). apply Qmult_lt_compat_r. rewrite <- H7. apply (strictly_order_preserving (cast AQ Q)), H6. rewrite <- H7. apply (strictly_order_preserving (cast AQ Q)), H5. 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