proposition: Lemma lexI x y z : (x <= y `&` z) = (x <= y) && (x <= z).
proof: Proof. rewrite !leEmeet; apply/eqP/andP => [<-|[/eqP<- /eqP<-]]. by rewrite meetA meetIK eqxx -meetA meetACA meetxx meetAC eqxx. by rewrite -[X in X `&` _]meetA meetIK meetA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)