fact: Definition is_neg (z: Z+nat) := match z with | inl (Zneg _) => true | _ => false end.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant