proposition: Lemma mulSgGid A x : x \in A -> A \subset G -> A * G = G.
proof: Proof. move=> Ax sAG; apply/eqP; rewrite eqEsubset -{2}mulGid mulSg //=. apply/subsetP=> y Gy; rewrite -(mulKVg x y) mem_mulg // groupMr // groupV. exact: (subsetP sAG). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)