proposition: Lemma cp_mid (z x y t : G) : t != z -> z \in cp x y -> exists (p1 : Path z x) (p2 : Path z y), t \notin p1 \/ t \notin p2.
proof: Proof. Proof using G_conn. move => tNz cp_z. case/connect_irredP : (G_conn x y) => p irr_p. move/cpP/(_ p) : cp_z. case/(isplitP irr_p) => p1 p2 A B C. exists (prev p1). exists p2. rewrite mem_prev. apply/orP. case E : (t \in p1) => //=. apply: contraNN tNz => F. by rewrite [t]C. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)