proposition: Fact meetA : associative meet.
proof: Proof. move=> x y z; apply: le_anti. apply/andP; split; rewrite !meetP -?andbA; apply/and3P; split. - exact: meet_leL. - exact: le_trans meet_leR meet_leL. - exact: le_trans meet_leR meet_leR. - exact: le_trans meet_leL meet_leL. - exact: le_trans meet_leL meet_leR. - exact: meet_leR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)