proposition: Lemma join_eq0 x y : (x `|` y == \bot) = (x == \bot) && (y == \bot).
proof: Proof. apply/idP/idP; last by move=> /andP [/eqP-> /eqP->]; rewrite joinx0. by move=> /eqP xUy0; rewrite -!lex0 -xUy0 leUl leUr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)