proposition: Lemma joins_disjoint I (d : L) (P : {pred I}) (F : I -> L) : (forall i : I, P i -> d `&` F i = \bot) -> d `&` \join_(i | P i) F i = \bot.
proof: Proof. move=> d_Fi_disj; have : \big[andb/true]_(i | P i) (d `&` F i == \bot). rewrite big_all_cond; apply/allP => i _ /=. by apply/implyP => /d_Fi_disj ->. elim/big_rec2: _ => [|i y]; first by rewrite meetx0. case; rewrite (andbF, andbT) // => Pi /(_ isT) dy /eqP dFi. by rewrite meetUr dy dFi joinxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)