proposition: Lemma Req_appart_dec : forall x y : R, { x = y } + { x < y \/ y < x }.
proof: Proof. intros. destruct (total_order_T x y). 1:destruct s. - right. left. exact r. - left. exact e. - right. right. exact r. Qed.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals