proposition: Lemma leU2E x y z t : x `&` t = \bot -> y `&` z = \bot -> (x `|` y <= z `|` t) = (x <= z) && (y <= t).
proof: Proof. move=> dxt dyz; apply/idP/andP; last by case=> ? ?; exact: leU2. by move=> lexyzt; rewrite (leU2l_le _ lexyzt) // (leU2r_le _ lexyzt). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)