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