proposition: Lemma Zgcd_pol_correct_lt : forall p env g c, Zgcd_pol p = (g,c) -> 0 < g -> eval_pol env p = g * (eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) + c.
proof: Proof. intros. rewrite <- Zdiv_pol_correct ; auto. - rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). unfold eval_pol. ring. - apply Zgcd_pol_div ; auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory