proposition: Lemma exists_arbitrarily_large_all (P : DS_set I -> Prop) : (forall i : DS_set I, P i) -> exists_arbitrarily_large P.
proof: Proof. intros HP i. exists i; split; auto. apply DS_ord_cond. Qed.
imports: ZornsLemma(Relation_Definitions_Implicit) Coq(Classical) Coq(Arith) Coq(Lia)