proposition: Lemma AR_mult_0_le_compat : ∀ x y : AR, ARle 0 x → ARle 0 y → ARle 0 (x*y).
proof: Proof. intros. apply ARtoCR_preserves_le. rewrite ARtoCR_preserves_mult. rewrite ARtoCR_preserves_0. apply (CRmult_le_0_compat ('x) ('y)). rewrite <- ARtoCR_preserves_0. apply ARtoCR_preserves_le, H5. rewrite <- ARtoCR_preserves_0. apply ARtoCR_preserves_le, H6. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring Coq.QArith.Qabs CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.util.Qdlog CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRArith CoRN.reals.fast.CRpower MathClasses.implementations.stdlib_binary_naturals MathClasses.orders.minmax MathClasses.implementations.positive_semiring_elements CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.AQmetric