proposition: Lemma is_neg_false : forall z, is_neg z = false -> (z_of_exp z >= 0)%Z.
proof: Proof. destruct z ; simpl ; try congruence. - destruct z ; try congruence. + compute. congruence. + compute. congruence. - generalize (Zle_0_nat n). auto using Z.le_ge. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant