proposition: Lemma cardSg_cyclic G H K : cyclic G -> H \subset G -> K \subset G -> (#|H| %| #|K|) = (H \subset K).
proof: Proof. move=> cycG sHG sKG; apply/idP/idP; last exact: cardSg. case/cyclicP: (cyclicS sKG cycG) => x defK; rewrite {K}defK in sKG *. case/dvdnP=> k ox; suffices ->: H :=: <[x ^+ k]> by apply: cycleX. apply/eqP; rewrite (eq_subG_cyclic cycG) ?(subset_trans (cycleX _ _)) //. rewrite -orderE orderXdiv orderE ox ?dvdn_mulr ?mulKn //. by have:= order_gt0 x; rewrite orderE ox; case k. 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)