proposition: Lemma meet_eq0E_diff z x y : x <= z -> (x `&` y == \bot) = (x <= z `\` y).
proof: Proof. move=> xz; apply/idP/idP; last by move=> /meet_r <-; rewrite -meetA meetBI. by move=> /eqP xIy_eq0; rewrite -[x](joinIB y) xIy_eq0 join0x leBl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)