proposition: Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0.
proof: Proof. unfold is_pol_Z0. intros p; destruct p as [z| |]; try discriminate. destruct z ; try discriminate. reflexivity. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory