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