fact: Definition IZR (z:Z) : R := match z with | Z0 => R0 | Zpos n => IPR n | Zneg n => - IPR n end.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals