proposition: Lemma cp_tightenR (x y z u : G) : z \in cp x y -> x \in cp u y -> x \in cp u z.
proof: Proof. Proof using G_conn. move=> z_cpxy x_cpuy. apply/cpP => pi. case/connect_irredP: (G_conn z y) => pi_o irred_o. move/cpP/(_ (pcat pi pi_o)): x_cpuy. rewrite mem_pcatT => /orP[//|x_tail]; exfalso. case: (altP (z =P y)). { move=> eq_z; move: pi_o irred_o x_tail. by rewrite -eq_z => pi_o /irredxx->. } case/(splitL pi_o) => [v] [zv] [pi'] [eq_pio eq_tail]. rewrite -{}eq_tail in x_tail. move: irred_o. rewrite eq_pio irred_edgeL => /andP[zNpi' Ipi']. move: zNpi'; apply/idP. case: (isplitP Ipi' x_tail) z_cpxy => [p1 p2 _ _ _] /cpP/(_ p2). by rewrite mem_pcat =>->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)