proposition: Lemma inject_Q_AR_plus : ∀ q r : Q, inject_Q_AR (q + r) = inject_Q_AR q + inject_Q_AR r.
proof: Proof. intros. apply (injective (Eembed QPrelengthSpace (cast AQ Q_as_MetricSpace))). pose proof CRAR_id as H5. unfold cast in H5. unfold ARtoCR, ARtoCR_uc in H5. unfold cast. rewrite (inject_Q_AR_CR (q+r)). rewrite (inject_Q_AR_CR q). rewrite (inject_Q_AR_CR r). unfold cast. unfold cast in H5. rewrite H5. pose proof (ARtoCR_preserves_plus (CRtoAR (' q)%CR) (CRtoAR (' r)%CR)) as H6. rewrite H6. rewrite <- CRplus_Qplus. apply ucFun2_wd. rewrite (H5 ('q)%CR). reflexivity. rewrite (H5 ('r)%CR). reflexivity. 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