proposition: Lemma Zdivide_pol_sub_0 : forall p a, Zdivide_pol a (PsubC Z.sub p 0) -> Zdivide_pol a p.
proof: Proof. intros p; induction p as [c|? p IHp|? IHp1 ? ? IHp2]. - simpl. intros ? H. inversion H. constructor. rewrite Z.sub_0_r in *. assumption. - intros ? H. constructor. simpl in H. inversion H ; subst; clear H. apply IHp ; auto. - simpl. intros ? H. inv H. constructor. + auto. + apply IHp2 ; assumption. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory