proposition: Lemma joing_idr A B : A <*> <<B>> = A <*> B.
proof: Proof. apply/eqP; rewrite eqEsubset gen_subG subUset gen_subG /=. by rewrite -subUset subset_gen genS // setUS // subset_gen. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)