proposition: Lemma cpPn x y z : reflect (exists2 p : Path x y, irred p & z \notin p) (z \notin cp x y).
proof: Proof. rewrite /cp -lock inE. apply: (iffP (separatorPn _ _ _)). - move => [x0] [y0] [p] [/set1P ? /set1P ?]; subst x0 y0. rewrite disjoint_sym disjoints1. by exists p. - move => [p Ip zNp]. exists x; exists y; exists (Build_IPath Ip). by rewrite disjoint_sym disjoints1 !inE !eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)