proposition: Theorem div_correct_factor: forall p a, (forall i, In i p -> P i) -> P a -> eval p a = zero -> forall x, P x -> eval p x = (mult (eval (fst (div p a)) x) (plus x (op a))).
proof: Proof. intros p a Hp Ha H x px. case (div_P p a); auto; intros Hd1 Hd2. rewrite (div_correct p a x); auto. generalize (div_correct p a a). rewrite plus_op_zero; try rewrite (fun x => mult_comm x zero); try rewrite mult_zero; try rewrite plus_zero; try rewrite H; auto. intros H1; rewrite <- H1; auto. rewrite (fun x => plus_comm x zero); auto. Qed.
imports: ZArith List UList Tactic Permutation