proposition: Lemma total_order_T : forall r1 r2:R, {Rlt r1 r2} + {r1 = r2} + {Rlt r2 r1}.
proof: Proof. intros. destruct (CRealLt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec). - left. left. rewrite RbaseSymbolsImpl.Rlt_def. apply CRealLtForget. exact c. - destruct (CRealLt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec). + right. rewrite RbaseSymbolsImpl.Rlt_def. apply CRealLtForget. exact c. + left. right. apply Rquot1. split; assumption. Qed.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals