fact: Definition Rinv : R -> R := fun x => match Req_appart_dec x R0 with | left _ => R0 | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r))) end.
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals