proposition: Lemma ex_imp_ex : forall (A:Type)(P Q:A->Prop), (ex P)->(forall x:A, P x -> Q x)->(ex Q).
proof: Proof. intros A P Q H H0; destruct H as [a Ha]. exists a; apply H0; assumption. Qed.
imports: ZArith List Arith ZArithRing Relations Lia