proposition: Lemma cycleP x y : reflect (exists i, y = x ^+ i) (y \in <[x]>).
proof: Proof. by apply: (iffP idP) => [/cyclePmin[i _]|[i ->]]; [exists i | apply: mem_cycle]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)