proposition: Lemma leBRL x y z : (x <= z `\` y) = (x <= z) && (x `&` y == \bot).
proof: Proof. apply/idP/idP => [xyz|]; first by rewrite (@meet_eq0E_diff z) // (le_trans xyz). by move=> /andP [?]; rewrite -meet_eq0E_diff. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)