proposition: Lemma Req_constr_leibniz : forall x y:R, Req_constr x y -> x = y.
proof: Proof. intros. destruct (total_order_T x y). 1:destruct s. - exfalso. destruct H. contradiction. - exact e. - exfalso. destruct H. contradiction. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms