proposition: Lemma RisLinearOrder : isLinearOrder Rlt.
proof: Proof. split. 1:split. - intros. exact (Rlt_asym _ _ H H0). - intros. exact (Rlt_trans _ _ _ H H0). - intros. destruct (total_order_T x y). + destruct s. * left. exact r. * right. subst x. exact H. + right. exact (Rlt_trans _ x _ r H). Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms