proposition: Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) -> Zdivide_pol y p.
proof: Proof. intros p x y H H0. induction H. - constructor. apply Z.divide_trans with (1:= H0) ; assumption. - constructor. auto. - constructor ; auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory