proposition: Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0.
proof: Proof. intros p; induction p as [c|p p1 IHp1|p1 IHp1 ? p3 IHp3]. 1-2: easy. simpl. case_eq (Zgcd_pol p1). case_eq (Zgcd_pol p3). intros. simpl. unfold ZgcdM. apply Z.le_ge; transitivity 1. - easy. - apply Z.le_max_r. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory