proposition: Lemma not_eal_eventually_not: forall (P: DS_set I -> Prop), ~ exists_arbitrarily_large P -> eventually (fun i:DS_set I => ~ P i).
proof: Proof. intros. apply not_all_ex_not in H. destruct H as [i]. exists i. intros. intro. contradiction H. exists j; split; trivial. Qed.
imports: ZornsLemma(Relation_Definitions_Implicit) Coq(Classical) Coq(Arith) Coq(Lia)