proposition: Lemma CRAR_id : forall x : CR, msp_eq (cast AR CR (cast CR AR x)) x.
proof: Proof. intro x. apply (surjective (Eembed QPrelengthSpace (cast AQ Q_as_MetricSpace)) x x). reflexivity. 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