proposition: Lemma right_arc x y p1 p2 (p := x :: p1 ++ y :: p2) : uniq p -> arc p y x = y :: p2.
proof: Proof. rewrite -[p]cat_cons -rot_size_cat rot_uniq => Up. by rewrite arc_rot ?left_arc ?mem_head. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)