proposition: Lemma cp_widenR (x y u v : G) : u \in cp x y -> v \in cp x u -> v \in cp x y.
proof: Proof. Abort. Lemma cp_widen (i o x y z : G) : x \in cp i o -> y \in cp i o -> z \in cp x y -> z \in cp i o. Proof using. move=> x_cpio y_cpio z_cpxy. apply: cpTI => p Ip. move: x_cpio y_cpio => /cpP/(_ p) x_p /cpP/(_ p) y_p. wlog : x y z_cpxy p Ip x_p y_p / x <[p] y. { move=> Hyp. case: (ltngtP (idx p x) (idx p y)); first exact: Hyp. - by apply: Hyp; first rewrite cp_sym. - move=>/(idx_inj x_p) x_y. by move: z_cpxy; rewrite -{1}x_y cpxx inE =>/eqP->. } case/(three_way_split Ip x_p y_p) => [p1][p2][p3][-> _ _]. rewrite !mem_pcat. by move: z_cpxy => /cpP/(_ p2)->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)