proposition: Lemma bag_interval_cap (x y z: G) (U : {set G}) : connected [set: G] -> x \in CP U -> y \in CP U -> z \in bag U x -> z \in interval x y -> z = x.
proof: Proof. move => conn_G xU yU Hz. rewrite /interval inE (disjointFr (interval_bag_disj _ _) Hz) // orbF. case/setUP => /set1P // ?. subst z. apply/eqP. by rewrite -(@bag_cp U). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)