proposition: Lemma interval_edge_cp (x y z u v : G) : z \in cp x y -> u -- v -> u \in interval x z -> v \in interval z y -> (u == z) || (v == z).
proof: Proof. Proof using. move=> z_cpxy uv u_xz v_zy. wlog [Hu Evy] : x y u v z_cpxy uv {u_xz v_zy} / u \in sinterval x z /\ v = y. { move=> Hyp. move: u_xz v_zy. rewrite !in_setU !in_set1 -!orbA. case/or3P=> [/eqP Eux|->//|Hu]; case/or3P=> [->//|/eqP Evy|Hv]. - move: uv; rewrite Eux Evy => xy. move/cpP/(_ (edgep xy)): z_cpxy. by rewrite mem_edgep ![z == _]eq_sym. - rewrite orbC. move: (conj Hv Eux). rewrite sinterval_sym. apply: Hyp; by rewrite 1?cp_sym 1?sg_sym. - by apply: Hyp (conj Hu Evy). - move: (sinterval_noedge_cp uv Hu Hv). by rewrite z_cpxy. } move: uv Hu; rewrite {}Evy inE => uy /andP[_]/cpPn[p _ zNp]. move/cpP/(_ (pcat (prev p) (edgep uy))): z_cpxy. by rewrite mem_pcat mem_prev mem_edgep (negbTE zNp) /= ![z == _]eq_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)