proposition: Lemma Zdivide_pol_sub : forall p a b, 0 < Z.gcd a b -> Zdivide_pol a (PsubC Z.sub p b) -> Zdivide_pol (Z.gcd a b) p.
proof: Proof. intros p; induction p as [c|? p IHp|p ? ? ? IHp2]. - simpl. intros a b H H0. inversion H0. constructor. apply Zgcd_minus ; auto. - intros ? ? H H0. constructor. simpl in H0. inversion H0 ; subst; clear H0. apply IHp ; auto. - simpl. intros a b H H0. inv H0. constructor. + apply Zdivide_pol_Zdivide with (1:= (ltac:(assumption) : Zdivide_pol a p)). destruct (Zgcd_is_gcd a b) ; assumption. + apply IHp2 ; assumption. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory