proposition: Lemma not_eventually_eal_not: forall (P: DS_set I -> Prop), ~ eventually P -> exists_arbitrarily_large (fun i:DS_set I => ~ P i).
proof: Proof. intros. red; intros. apply NNPP; intro. contradiction H. exists i. intros. apply NNPP; intro. contradiction H0. now exists j. Qed.
imports: ZornsLemma(Relation_Definitions_Implicit) Coq(Classical) Coq(Arith) Coq(Lia)