proposition: Lemma arc_path x y (xDy : x != y) : ucycle e s -> x \in s -> y \in s -> path0 e (arc s x y).
proof: Proof. move=> /andP[cycle_s uniq_s] x_s y_s. have [i s1 s2 <- _ E /=] := rot_to_arc uniq_s x_s y_s xDy. move: cycle_s. rewrite -(rot_cycle i) E /= rcons_path cat_path. by case: (path e x s1). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)