fact: Definition IQmake_to_decimal num den := match den with | 1%positive => None | _ => IQmake_to_decimal num den end.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals