proposition: Lemma inject_Q_AR_CR : forall (q : Q), inject_Q_AR q = cast CR AR (inject_Q_CR q).
proof: Proof. intro q. rewrite <- doubleSpeed_Eq. intros e1 e2. rewrite Qplus_0_r. pose proof (regFun_prf (cast CR AR (inject_Q_CR q)) e1 e2) as H5. apply H5. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring CoRN.util.Qdlog CoRN.model.totalorder.QposMinMax CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.metric2.MetricMorphisms CoRN.reals.faster.ApproximateRationals