fact: Definition to_number q := match to_decimal q with | None => None | Some q => Some (Number.Decimal q) end.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals