proposition: Theorem div_P: forall p a, P a -> (forall i, In i p -> P i) -> (forall i, In i (fst (div p a)) -> P i) /\ P (snd (div p a)).
proof: Proof. intros p a Pa; elim p; auto with datatypes. intros a1 l1; case l1. simpl; intuition. intros a2 p2 Rec Hi; split. case Rec; auto with datatypes. intros H H1 i. replace (In i (fst (div (a1 :: a2 :: p2) a))) with (snd (div (a2::p2) a) = i \/ In i (fst (div (a2::p2) a))); auto. intros [Hi1 | Hi1]; auto. rewrite <- Hi1; auto. change ( P (plus a1 (mult a (snd (div (a2::p2) a))))); auto with datatypes. apply Pplus; auto with datatypes. apply Pmult; auto with datatypes. case Rec; auto with datatypes. Qed.
imports: ZArith List UList Tactic Permutation