proposition: Lemma CRltT_linear : @isLinearOrder (RegularFunction Qball) CRltT.
proof: Proof. split. split. - intros. apply (CRlt_trans _ _ _ H) in H0. apply (CRlt_irrefl x H0). - intros. exact (CRlt_trans _ _ _ H H0). - apply CRlt_linear. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon