proposition: Lemma joinA : associative join.
proof: Proof. by move=> x y z; rewrite -{1}[x]set_join1 -set_joinU setUA set_joinU set_join1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)