proposition: Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p.
proof: Proof. intros p; induction p as [c| |]; constructor ; auto. exists c. ring. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory