fact: Definition z_of_exp (z : Z + nat) := match z with | inl z => z | inr n => Z.of_nat n end.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant