proposition: Lemma interval_bag_edges_disj (G : graph) (U : {set G}) (x y : G) : connected [set: skeleton G] -> x \in @CP (skeleton G) U -> y \in @CP (skeleton G) U -> [disjoint edge_set (@bag G U x) & @interval_edges G x y].
proof: Proof. move=> G_conn x_cp y_cp. rewrite -setI_eq0 -subset0. apply/subsetP => e. rewrite 3!inE => /and3P[]/andP[src_p tgt_p]. rewrite 4!inE ![_ \in @interval G _ _]inE (lock sinterval) !inE -lock. rewrite negb_or !negb_and -!orbA => /andP[eNx eNy]. case/andP=> /or3P[src_x|src_y|src_sI] /or3P[tgt_x|tgt_y|tgt_sI]. all: move: eNx eNy; rewrite ?src_x ?src_y ?tgt_x ?tgt_y ?orbF //= => eNx eNy. - move: eNx. by rewrite (eqP tgt_y) -(@bag_cp G _ U) // -(eqP tgt_y) tgt_p. - by case: (disjointE (@interval_bag_disj G U x y y_cp) tgt_p tgt_sI). - move: eNx. by rewrite (eqP src_y) -(@bag_cp G _ U) // -(eqP src_y) src_p. - by case: (disjointE (@interval_bag_disj G U x y y_cp) tgt_p tgt_sI). - by case: (disjointE (@interval_bag_disj G U x y y_cp) src_p src_sI). - by case: (disjointE (@interval_bag_disj G U x y y_cp) src_p src_sI). - by case: (disjointE (@interval_bag_disj G U x y y_cp) src_p src_sI). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)