proposition: Lemma meet_eq1 x y : (x `&` y == \top) = (x == \top) && (y == \top).
proof: Proof. apply/idP/idP; last by move=> /andP[/eqP-> /eqP->]; rewrite meetx1. by move=> /eqP xIy1; rewrite -!le1x -xIy1 leIl leIr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)