fact: Definition Req_constr (x y : R) : Prop := (x < y -> False) /\ (y < x -> False).
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms