proposition: Lemma tree_I3 (T : 'I_3 -> {set G}) : (forall i, connected (T i)) -> (forall i j, T i :&: T j != set0) -> exists z, forall i, z \in T i.
proof: Proof. move => tree_T T_pw_in. case/set0Pn : (T_pw_in ord0 ord1) => x /setIP [X0 X1]. case/set0Pn : (T_pw_in ord0 ord2) => y /setIP [Y0 Y1]. case: (path_in_connected _ X0 Y0) => [|p irr_p /subsetP sub_T0]; first exact: tree_T. case: (@subtree_cut (T ord1) (T ord2) x y p) => // z [/sub_T0 ? ? ?]. exists z. exact: ord3P. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph set_tac)