proposition: Lemma subtree_cut (T1 T2 : {set G}) (x1 x2 : G) (p : Path x1 x2) : connected T1 -> connected T2 -> T1 :&: T2 != set0 -> x1 \in T1 -> x2 \in T2 -> irred p -> exists y, [/\ y \in p, y \in T1 & y \in T2].
proof: Proof. move => tree_T1 tree_T2 cap_T12 X11 X22 Ip. case/set0Pn : cap_T12 => z /setIP [Z1 Z2]. move: p Ip. move def_A : (T1 :&: T2) => A. have zA : z \in A by rewrite -def_A inE Z1. gen have H,Hp1 : T1 T2 x1 x2 tree_T1 tree_T2 X11 X22 Z1 Z2 def_A zA / exists z1 (p1 : Path x1 z1), [/\ z1 \in A, irred p1, p1 \subset T1 & forall k, k \in A -> k \in p1 -> k = z1]. { case: (@path_in_connected _ T1 x1 z) => // p1 Ip1 subT1. case: (split_at_first zA (path_end p1)) => z1 [p11] [p12] [E H1 H2]. subst. exists z1. exists p11. split => //. + by case/irred_catE : Ip1. + apply: subset_trans subT1. exact: subset_pcatL. } move: Hp1 => [z1] [p1] [zA1 Ip1 /subsetP sub_p1 H1]. case: (H T2 T1 x2 x1) => // {H}; first by rewrite setIC. move => z2 [p2] [zA2 Ip2 /subsetP sub_p2 H2]. case: (path_in_connected _ zA1 zA2) => [|q Iq /subsetP qA]. { rewrite -def_A. exact: tree_connectI. } set r := pcat (pcat p1 q) (prev p2). suff I: irred r. { move => p Ip. have -> : p = r by apply: forestT_unique. exists z1. rewrite !inE /= -def_A in zA1 *. by case/setIP : zA1 => -> -> . } rewrite /r. apply: irred_catI. - move => k. rewrite !inE. case/orP => U V. + rewrite [k]H2 //. by rewrite -def_A inE sub_p1 ?sub_p2. + by rewrite [k]H2 // qA. - apply: irred_catI => // k ? /qA ?. exact: H1. - by rewrite irred_rev. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph set_tac)