proposition: Lemma head_arc (T: eqType) (s : seq T) (x y : T) (xDy : x != y) : uniq s -> x \in s -> y \in s -> x \in arc s x y.
proof: Proof. move=> uniq_s x_s y_s. case: (rot_to_arc uniq_s x_s y_s xDy) => i s1 s2 <- _ _. exact: mem_head. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)