fact: Definition is_pol_Z0 (p : PolC Z) : bool := match p with | Pc Z0 => true | _ => false end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory