proposition: Lemma arc_rot i p : uniq p -> {in p, arc (rot i p) =2 arc p}.
proof: Proof. move=> Up x p_x y; congr (fun q => take (index y q) q); move: Up p_x {y}. rewrite -{1 2 5 6}(cat_take_drop i p) /rot cat_uniq => /and3P[_ Up12 _]. rewrite !drop_cat !take_cat !index_cat mem_cat orbC. case p2x: (x \in drop i p) => /= => [_ | p1x]. rewrite index_mem p2x [x \in _](negbTE (hasPn Up12 _ p2x)) /= addKn. by rewrite ltnNge leq_addr catA. by rewrite p1x index_mem p1x addKn ltnNge leq_addr /= catA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)