proposition: Lemma diffIx x y z : (x `&` y) `\` z = (x `\` z) `&` (y `\` z).
proof: Proof. apply/eqP; rewrite eq_diff joinIr ?leI2 ?diffKU ?leUr ?leBx //=. by rewrite -meetA diffIK meetx0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)