proposition: Lemma finI_from_join A B t : finI_from A -> finI_from B -> A t -> B t -> exists k, [/\ finI_from k, k t & k `<=` A `&` B].
proof: Proof. move=> [DA sDAD AeIbA] [DB sDBD BeIbB] At Bt. exists (A `&` B); split => //. exists (DA `|` DB)%fset; first by move=> i /fsetUP [/sDAD|/sDBD]. rewrite predeqE => s; split=> [Ifs|[As Bs] i /fsetUP]. split; first by rewrite -AeIbA => i DAi; apply: Ifs; rewrite /= inE DAi. by rewrite -BeIbB => i DBi; apply: Ifs; rewrite /= inE DBi orbC. by move=> [DAi|DBi]; [have := As; rewrite -AeIbA; apply|have := Bs; rewrite -BeIbB; apply]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed