proposition: Lemma eventually_impl: forall (P Q: DS_set I -> Prop), eventually P -> eventually (fun i:DS_set I => P i -> Q i) -> eventually Q.
proof: Proof. intros. apply eventually_impl_base with (P := fun (i:DS_set I) => P i /\ (P i -> Q i)). - tauto. - now apply eventually_and. Qed.
imports: ZornsLemma(Relation_Definitions_Implicit) Coq(Classical) Coq(Arith) Coq(Lia)