proposition: Lemma arc_subcycle_disjoints (T : finType) (p s : seq T) (x y nx ny : T) : uniq s -> subcycle p s -> x \in p -> y \in p -> x != y -> nx = next p x -> ny = next p y -> [disjoint [set z in arc s x nx] & [set z in arc s y ny]].
proof: Proof. move=> uniq_s subcycle_p x_p y_p xDy next_x next_y. under eq_disjoint => z do by rewrite !inE. under eq_disjoint_r => z do by rewrite !inE. by rewrite next_x next_y; apply: (arc_subcycle_disjoint uniq_s). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)