proposition: Lemma cycleX x i : <[x ^+ i]> \subset <[x]>.
proof: Proof. by rewrite cycle_subG; apply: mem_cycle. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)