proposition: Lemma isog_cyclic_card G M : cyclic G -> isog G M = cyclic M && (#|M| == #|G|).
proof: Proof. move=> cycG; apply/idP/idP=> [isoGM | ]. by rewrite (card_isog isoGM) -(isog_cyclic isoGM) cycG /=. case/cyclicP: cycG => x ->{G} /andP[/cyclicP[y ->] /eqP oy]. by apply: isog_trans (isog_symr _) (Zp_isog y); rewrite /order oy Zp_isog. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)