proposition: Lemma Zgcd_pol_div : forall p g c, Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c).
proof: Proof. intros p; induction p as [c|? ? IHp|p1 IHp1 ? p3 IHp2]; simpl. - intros ? ? H. inv H. constructor. exists 0. now ring. - intros. constructor. apply IHp ; auto. - intros g c. case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1. inv H1. unfold ZgcdM at 1. destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; destruct HH1 as [HH1 HH1'] ; rewrite HH1'. + constructor. * apply (Zdivide_pol_Zdivide _ (ZgcdM z1 z2)). -- unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. ++ destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_sub ; auto. apply Z.lt_le_trans with 1. ** reflexivity. ** now apply Z.ge_le. ++ destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_one. -- unfold ZgcdM in HH1. unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. ++ destruct HH2 as [H1 H2]. rewrite H2 in *. destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto. ++ destruct HH2 as [H1 H2]. rewrite H2. destruct (Zgcd_is_gcd 1 z); auto. * apply (Zdivide_pol_Zdivide _ z). -- apply (IHp2 _ _ H); auto. -- destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto. + constructor. * apply Zdivide_pol_one. * apply Zdivide_pol_one. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory