proposition: Lemma card_isog : G \isog H -> #|G| = #|H|.
proof: Proof. by case/isogP=> f injf <-; apply: isom_card (f) _; apply/isomP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)