proposition: Lemma cycle_catC p q : cycle (p ++ q) = cycle (q ++ p).
proof: Proof. case: p q => [|x p] [|y q]; rewrite /= ?cats0 //=. by rewrite !rcons_path !cat_path !last_cat /= -!andbA; do !bool_congr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)