proposition: Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p -> forall env, eval_pol env p = a * eval_pol env (Zdiv_pol p a).
proof: Proof. intros a p H H0. induction H0 as [? ?|? ? IHZdivide_pol j|? ? ? IHZdivide_pol1 ? IHZdivide_pol2 j]. - simpl. intros. apply Zdivide_Zdiv_eq ; auto. - simpl. intros. apply IHZdivide_pol. - simpl. intros. rewrite IHZdivide_pol1. rewrite IHZdivide_pol2. ring. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory