proposition: Lemma arc_remainder x : 1 < size p -> x \in p -> {subset p <= rcons (arc s (next p x) x) x}.
proof: Proof. move=> gt1p x_p y y_p; rewrite mem_rcons inE; have [//|xDy/=] := eqVneq x y. rewrite mem_arc_other ?p_in_s ?mem_next // 1?eq_sym ?next_neq //. have D := arc_next_disjoint x_p y_p xDy. by rewrite (disjointFl D) // head_arc ?p_in_s ?next_neq ?mem_next. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)