proposition: Lemma subcycleP p s : reflect (exists n, subseq (rot n p) s) (subcycle p s).
proof: Proof. apply: (iffP existsP) => [[n On]|[n rot_n]]; first by exists n. have [lt_p|ge_p] := ltnP n (size p).+1; first by exists (Ordinal lt_p). by exists (Ordinal (ltn0Sn _)); rewrite /= rot0 -[p](@rot_oversize _ n) // ltnW. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)