proposition: Lemma left_arc x y p1 p2 (p := x :: p1 ++ y :: p2) : uniq p -> arc p x y = x :: p1.
proof: Proof. rewrite /arc /p [index x _]/= eqxx rot0 -cat_cons cat_uniq index_cat. move: (x :: p1) => xp1 /and3P[_ /norP[/= /negbTE-> _] _]. by rewrite eqxx addn0 take_size_cat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)