proposition: Lemma link_avoid (x y z : G) : z \notin [set x; y] -> link_rel x y -> exists2 p, pathp x y p & z \notin (x::p).
proof: Proof. Abort. Lemma link_seq_cp (y x : G) p : @pathp link_graph x y p -> cp x y \subset x :: p. Proof using. elim: p x => [|z p IH] x /=. - move/pathp_nil->. rewrite cpxx. apply/subsetP => z. by rewrite !inE. - rewrite pathp_cons => /andP [/= /andP [A B] /IH C]. apply: subset_trans (cp_triangle z) _. rewrite subset_seqR. apply/subUsetP; split. + apply: subset_trans B _. by rewrite !set_cons setUA subsetUl. + apply: subset_trans C _. by rewrite set_cons subset_seqL subsetUr. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)