proposition: Lemma interval_bag_edge_cover (G : graph) (x y : G) : connected [set: skeleton G] -> x != y -> [set: edge G] = edge_set (@bag G [set x; y] x) :|: @interval_edges G x y :|: edge_set (@bag G [set x; y] y).
proof: Proof. move=> G_conn xNy. apply/eqP. rewrite eq_sym -subTset. apply/subsetP=> e _. move: (sinterval_bag_cover G_conn xNy) => compU. have : target e \in [set: G] by []. have : source e \in [set: G] by []. rewrite !{}compU !in_setU -!orbA. case: (boolP (source e \in @sinterval G x y)) => [Hsrc _|Nsrc /= Hsrc]. + case: (boolP (target e \in @sinterval G x y)) => [Htgt _|Ntgt /= Htgt]. { rewrite ![e \in _]inE ![_ \in @interval G _ _]inE Hsrc Htgt. rewrite !orbT negb_or !negb_and. suff [-> ->] : source e != x /\ source e != y by []. by split; apply: contraTneq Hsrc => ->; rewrite (@sinterval_bounds G). } wlog Htgt : x y xNy Hsrc Ntgt {Htgt} / target e \in @bag G [set x; y] x. { move=> Hyp. case/orP: Htgt; first exact: Hyp. rewrite setUC orbC orbAC orbC interval_edges_sym. apply: Hyp; rewrite 1?sinterval_sym //. by rewrite eq_sym. } have Nsrc : source e \notin @bag G [set x; y] x. { rewrite (disjointFl (@interval_bag_disj G _ x y _) Hsrc) //. apply: CP_extensive. by rewrite !inE eqxx. } have src_tgt : @sedge G (target e) (source e). { rewrite /=/sk_rel adjacent_sym adjacent_edge andbT. by apply: contraNneq Ntgt =>->. } have : target e = x := bag_exit_edge G_conn _ Htgt Nsrc src_tgt. move/(_ (CP_extensive _)). rewrite 3!inE eqxx => /(_ _)/Wrap[]// tgt_x. rewrite ![e \in _]inE tgt_x (@intervalL G) [_ \in @interval G _ _]inE Hsrc. rewrite orbT !andbT negb_or !negb_and. suff [->->] : source e != x /\ source e != y by []. by split; apply: contraTneq Hsrc =>->; rewrite (@sinterval_bounds G). + wlog Hsrc : x y xNy {Nsrc Hsrc} / source e \in @bag G [set x; y] x. { move=> Hyp. case/orP: Hsrc; first exact: Hyp. rewrite setUC sinterval_sym interval_edges_sym orbC orbAC orbC. rewrite [(e \in _) || _]orbC orbAC [_ || (e \in _)]orbC. by apply: Hyp; rewrite eq_sym. } case: (boolP (target e \in @bag G [set x; y] x)) => Ntgt /=. by rewrite [e \in _]inE Hsrc Ntgt. have src_tgt : @sedge G (source e) (target e). { rewrite /=/sk_rel adjacent_edge andbT. by apply: contraNneq Ntgt =><-. } have : source e = x := bag_exit_edge G_conn _ Hsrc Ntgt src_tgt. move/(_ (CP_extensive _)). rewrite 3!inE eqxx => /(_ _)/Wrap[]// src_x. case/orP=> Htgt. * rewrite ![e \in _]inE src_x (@intervalL G) (negbTE xNy) orbF eqxx/=. have -> : target e != x. { apply: contraTneq Htgt =>->. by rewrite (@sinterval_bounds G). } by have -> : target e \in @interval G x y by rewrite inE Htgt. * have Nsrc : source e \notin @bag G [set x; y] y. { have yNx : y != x by rewrite eq_sym. rewrite (disjointFl (bag_disj G_conn _ _ yNx) Hsrc) //; by apply: CP_extensive; rewrite !inE eqxx. } have := bag_exit_edge G_conn (CP_extensive _) Htgt Nsrc _. rewrite sg_sym 3!inE eqxx => /(_ _ src_tgt)/Wrap[]// tgt_y. rewrite ![e \in _]inE src_x tgt_y (@intervalL G) (@intervalR G). by rewrite !eqxx eq_sym (negbTE xNy). 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)