proposition: Lemma filter_ex2 {T U : Type} (F : set_system T) (G : set_system U) {FF : ProperFilter F} {FG : ProperFilter G} (P : set T) (Q : set U) : F P -> G Q -> exists x : T, exists2 y : U, P x & Q y.
proof: Proof. by move=> /filter_ex [x Px] /filter_ex [y Qy]; exists x, y. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed