proposition: Lemma extnprod_mul1g : left_id [ffun=> 1%g] extnprod_mulg.
proof: Proof. by move=> x; apply/ffunP => i; rewrite !ffunE mul1g. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)