proposition: Lemma connect_cycle p : cycle e p -> {in p &, forall x y, connect x y}.
proof: Proof. move=> e_p x y /rot_to[i q rip]; rewrite -(mem_rot i) rip => yqx. have /= : cycle e (x :: q) by rewrite -rip rot_cycle. case/splitPl: yqx => r s lxr; rewrite rcons_cat cat_path => /andP[xr _]. by apply/connectP; exists r. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)