proposition: Lemma rot_to_arc p x y : uniq p -> x \in p -> y \in p -> x != y -> rot_to_arc_spec p x y.
proof: Proof. move=> Up p_x p_y ne_xy; case: (rot_to p_x) (p_y) (Up) => [i q def_p] q_y. rewrite -(mem_rot i) def_p inE eq_sym (negbTE ne_xy) in q_y. rewrite -(rot_uniq i) def_p. case/splitPr: q / q_y def_p => q1 q2 def_p Uq12; exists i q1 q2 => //. by rewrite -(arc_rot i Up p_x) def_p left_arc. by rewrite -(arc_rot i Up p_y) def_p right_arc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)