proposition: Lemma all_not_ex_func (A : Type) (P Q : A -> Prop) : (forall x, Q x -> ~P x) -> (forall x, Q x) -> (~exists x, P x).
proof: Proof. intros allx_Qx_to_notPx allx_Qx. apply all_not_not_ex. intro x. exact ((allx_Qx_to_notPx x) (allx_Qx x)). Qed.
imports: Classical_Prop Classical_Pred_Type