proposition: Lemma ARltS_linear : @isLinearOrder (RegularFunction (Eball (cast AQ Q))) ARltS.
proof: Proof. destruct ARfpsro, full_pseudo_srorder_pso. destruct pseudo_srorder_strict. split. split. - intros x y J J0. pose proof (AR_lt_ltT x y) as [_ J1]. pose proof (AR_lt_ltT y x) as [_ J2]. exact (pseudo_order_antisym x y (conj (J1 J) (J2 J0))). - intros. destruct (ARtoCR_preserves_ltT x z) as [_ a]. apply a. clear a. destruct (ARtoCR_preserves_ltT x y) as [a _]. apply a in H5. clear a. destruct (ARtoCR_preserves_ltT y z) as [a _]. apply a in H6. apply (CRlt_trans _ _ _ H5 H6). - intros x y z J. destruct (CRlt_linear (cast AR CR x) (cast AR CR y) (cast AR CR z)). apply (ARtoCR_preserves_ltT x z), J. left. destruct (ARtoCR_preserves_ltT x y). apply a, c. right. destruct (ARtoCR_preserves_ltT y z). apply a, c. 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