proposition: Lemma isog_eq1 : G \isog H -> (G :==: 1) = (H :==: 1).
proof: Proof. by move=> isoGH; rewrite !trivg_card1 card_isog. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)