proposition: Lemma interval_cp_cover x y z : z \in cp x y :\: [set x; y] -> interval x y = (x |: sinterval x z) :|: bag [set x; y] z :|: (y |: sinterval z y).
proof: Proof. Proof using G_conn. rewrite /interval => /sinterval_cp_cover->. by rewrite setUAC -setUA [_ :|: set1 y]setUAC !setUA. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)