proposition: Lemma eventually_and: forall (P Q: DS_set I -> Prop), eventually P -> eventually Q -> eventually (fun i:DS_set I => P i /\ Q i).
proof: Proof. intros. destruct H, H0. destruct (DS_join_cond x x0) as [? [? ?]]. exists x1. intros; split; [ apply H | apply H0 ]; apply preord_trans with x1; trivial; apply DS_ord_cond. Qed.
imports: ZornsLemma(Relation_Definitions_Implicit) Coq(Classical) Coq(Arith) Coq(Lia)