proposition: Lemma leI2E x y z t : x `|` t = \top -> y `|` z = \top -> (x `&` y <= z `&` t) = (x <= z) && (y <= t).
proof: Proof. by move=> ? ?; apply: (@leU2E _ L^d); rewrite meetC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)