proposition: Lemma setXn_group_set n (gT : 'I_n -> finGroupType) (G : forall i, {group gT i}) : group_set (setXn G).
proof: Proof. apply/andP => /=; split. by rewrite inE; apply/forallP => i; rewrite ffunE group1. apply/subsetP => x /mulsgP[u v]; rewrite !inE => /forallP uG /forallP vG {x}->. by apply/forallP => x; rewrite ffunE groupM ?uG ?vG. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)