proposition: Lemma joing_idPl G A : reflect (G <*> A = G) (A \subset G).
proof: Proof. apply: (iffP idP) => [sHG | <-]; last by rewrite joing_subr. by rewrite joingE (setUidPl sHG) genGid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)