proposition: Lemma indexMg G A : #|G * A : G| = #|A : G|.
proof: Proof. apply/eq_card/setP/eqP; rewrite eqEsubset andbC imsetS ?mulG_subr //. by apply/subsetP=> _ /rcosetsP[x GAx ->]; rewrite mem_rcosets. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)