proposition: Lemma arc_edge x y : ucycle e s -> x \in s -> y \in s -> x != y -> e (last x (arc s x y)) y.
proof: Proof. move => /andP [cycle_s uniq_s] x_s y_s xDy. have [n s1 s2 <- _ rot_s] := rot_to_arc uniq_s x_s y_s xDy. move: cycle_s; rewrite -(rot_cycle n) {}rot_s /=. by rewrite rcons_path cat_path /=; case: (e (last _ _) _); rewrite // andbF. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)