proposition: Lemma not_all_not_ex : forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n.
proof: Proof. intros P notall. apply NNPP. intro abs. apply notall. intros n H. apply abs; exists n; exact H. Qed.
imports: Classical_Prop