proposition: Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) : (forall x:A, {P x} + { ~ P x }) -> ~ Forall P l -> Exists (fun x => ~ P x) l.
proof: Proof. intro Dec. apply Exists_Forall_neg; intros x. destruct (Dec x); auto. Qed.
imports: PeanoNat