proposition: Lemma eq_subG_cyclic G H K : cyclic G -> H \subset G -> K \subset G -> (H :==: K) = (#|H| == #|K|).
proof: Proof. case/cyclicP=> x -> sHx sKx; apply/eqP/eqP=> [-> //| eqHK]. have def_GHx := cycle_sub_group (cardSg sHx); set GHx := [set _] in def_GHx. have []: H \in GHx /\ K \in GHx by rewrite -def_GHx !inE sHx sKx eqHK /=. by do 2!move/set1P->. 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)