proposition: Lemma interval_bag_disj U (x y : G) : y \in CP U -> [disjoint bag U x & sinterval x y].
proof: Proof. Proof using. move => Uy. rewrite disjoint_sym disjoints_subset. apply/subsetP => z. rewrite !inE => /andP[A1 A2]. apply: contraTN A1 => /bagP/(_ _ Uy). by rewrite negbK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)