proposition: Lemma link_path_cp (x y : G) (p : @Path link_graph x y) : {subset cp x y <= p}.
proof: Proof. Proof using. apply/subsetP. rewrite /in_nodes nodesE. apply: link_seq_cp. exact: (valP p). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)