fact: Definition IPR (p:positive) : R := match p with | xH => R1 | xO p => IPR_2 p | xI p => R1 + IPR_2 p end.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals