proposition: Lemma arc_cover x y : x \in s -> y \in s -> x != y -> s =i [predU arc s x y & arc s y x].
proof: Proof. move=> x_s y_s xDy z; have [i s1 s2 A1 A2 def_s] := rot_to_arc uniq_s x_s y_s xDy. by rewrite -(mem_rot i) def_s -cat_cons A1 A2 mem_cat. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)