proposition: Lemma cp_tighten (i o p x y : G) : i \in cp x p -> o \in cp p y -> p \in cp x y -> p \in cp i o.
proof: Proof. Abort. Lemma cp_neighbours (x y : G) z : x != y -> (forall x' (p : Path x' y), x -- x' -> irred p -> x \notin p -> z \in p) -> z \in cp x y. Proof using. move=> xNy H. apply: cpTI => p. case: (splitL p xNy) => [x'] [xx'] [p'] [-> _]. rewrite irred_edgeL => /andP[xNp' Ip]. by rewrite mem_pcat H. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)