proposition: Lemma intervalI_cp (x y z : G) : z \in cp x y -> interval x z :&: interval z y = [set z].
proof: Proof. Proof using. move=> z_cpxy. apply/setP=> u. rewrite [LHS]inE ![_ \in interval _ _]inE (lock sinterval) !inE -lock -!orbA. apply/idP/idP; last by move=>->. case/andP=> /or3P[/eqP->|->//|u_sIxz] /or3P[->//|/eqP u_y|u_sIzy]. - move: z_cpxy. by rewrite -u_y cpxx inE eq_sym. - move: u_sIzy. by rewrite inE z_cpxy. - move: u_sIxz. by rewrite u_y inE (cp_sym y x) z_cpxy andbF. - by case: (disjointE (sinterval_disj_cp z_cpxy) u_sIxz u_sIzy). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)