proposition: Lemma is_neg_true : forall z, is_neg z = true -> (z_of_exp z < 0)%Z.
proof: Proof. destruct z ; simpl ; try congruence. destruct z ; try congruence. intros. reflexivity. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant