proposition: Lemma AR_zero : msp_eq (inject_Q_AR 0) (cast AQ AR zero0).
proof: Proof. pose proof (ARtoCR_inject zero0) as H5. unfold cast in H5. unfold cast. rewrite inject_Q_AR_CR. apply (injective ARtoCR). rewrite H5. pose proof CRAR_id as H6. unfold cast in H6. rewrite (H6 (0%CR)). apply inject_Q_CR_wd. symmetry. apply rings.preserves_0. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.reals.faster.ARArith CoRN.reals.faster.ARabs CoRN.metric2.Metric CoRN.metric2.Complete CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs ConstructiveFastReals