proposition: Lemma diffxU x y z : z `\` (x `|` y) = (z `\` x) `&` (z `\` y).
proof: Proof. apply/eqP; rewrite eq_le lexI !leBr ?leUl ?leUr //=. rewrite leBRL leIx2 ?leBx //= meetUr meetAC diffIK -meetA diffIK. by rewrite meet0x meetx0 joinx0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)