proposition: Lemma sinterval_bag_cover x y : x != y -> [set: G] = bag [set x; y] x :|: sinterval x y :|: bag [set x; y] y.
proof: Proof. Proof using G_conn. move=> xNy. apply/eqP. rewrite eqEsubset subsetT andbT. apply/subsetP => p _. rewrite setUAC setUC !in_setU inE -negb_or -implybE. apply/implyP. wlog suff Hyp : x y {xNy} / x \in cp p y -> p \in bag [set x; y] x. { by case/orP => /Hyp; last rewrite setUC; move=>->. } move=> x_cppy; apply/bagP => z. rewrite CP_set2 => z_cpxy. exact: cp_tightenR z_cpxy x_cppy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)