proposition: Lemma CRealLtIsLinear : isLinearOrder CRealLt.
proof: Proof. repeat split. - exact CRealLt_asym. - exact CReal_lt_trans. - intros. destruct (CRealLt_dec x z y H). + left. exact c. + right. exact c. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax