proposition: Lemma AR_lt_0_1 : ARltT (inject_Q_AR 0) (inject_Q_AR 1).
proof: Proof. pose proof (inject_Q_AR_CR 0). pose proof (inject_Q_AR_CR 1). symmetry in H5. symmetry in H6. apply (ARltT_wd _ _ H5 _ _ H6). destruct (CRtoAR_preserves_ltT 0%CR 1%CR). exact (a (CRlt_Qlt 0 1 eq_refl)). 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