proposition: Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0.
proof: Proof. intros x; destruct x ; simpl ; intuition congruence. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory