proposition: Lemma bag_sub_sinterval (U : {set G}) x y z : x \in CP U -> y \in CP U -> z \in cp x y :\: [set x; y] -> bag U z \subset sinterval x y.
proof: Proof. Proof using G_conn. rewrite in_setD in_set2 negb_or => x_cp y_cp /andP[]/andP[zNx zNy] z_cpxy. apply/subsetP=> u /bagP u_bag. move: x_cp y_cp => /u_bag z_cpux /u_bag z_cpuy. rewrite inE. apply/andP; split. - apply: contraNN zNx => x_cpuy. suff : x \in cp z z by rewrite cpxx in_set1 eq_sym. suff : x \in cp z u by apply: cp_tightenR; rewrite cp_sym. rewrite cp_sym; exact: cp_tightenR z_cpxy x_cpuy. - apply: contraNN zNy => y_cpux. suff : y \in cp z z by rewrite cpxx in_set1 eq_sym. suff : y \in cp z u by apply: cp_tightenR; rewrite cp_sym. rewrite cp_sym; apply: cp_tightenR y_cpux; by rewrite cp_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)