proposition: Lemma AR_mult_0_lt_compat : ∀ x y : AR, ARltT (inject_Q_AR 0) x → ARltT (inject_Q_AR 0) y → ARltT (inject_Q_AR 0) (ARmult x y).
proof: Proof. intros x y X X0. destruct (ARtoCR_preserves_ltT (inject_Q_AR 0) (ARmult x y)) as [_ a]. apply a. clear a. pose proof (ARtoCR_preserves_mult x y) as H5. unfold mult in H5. symmetry in H5. assert (0 = ARtoCR (inject_Q_AR 0))%CR as H7. { rewrite <- (CRAR_id 0%CR). unfold cast. rewrite (inject_Q_AR_CR 0). reflexivity. } pose proof (ARtoCR_preserves_mult x y) as H8. symmetry in H8. apply (CRltT_wd H7 H8). clear H8 H5. apply CRmult_lt_0_compat. - destruct (ARtoCR_preserves_ltT (inject_Q_AR 0) x). apply c in X. clear a c. symmetry in H7. apply (CRltT_wd H7 (reflexivity _)). exact X. - destruct (ARtoCR_preserves_ltT (inject_Q_AR 0) y). apply c in X0. clear a c. symmetry in H7. apply (CRltT_wd H7 (reflexivity _)). exact X0. 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