fact: Definition Rlt : R -> R -> Prop := fun x y : R => CRealLtProp (Rrepr x) (Rrepr y).
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals