proposition: Lemma connector_sep P A B n (p q : 'I_n -> pathS G) i j x : separator A B P -> connector A P p -> connector P B q -> x \in p i -> x \in q j -> (x \in P) .
proof: Proof. move => sep_P con_p con_q x_pi x_qj. case def_pi : (p i) => [[u v] /= pi]. case def_qj : (q j) => [[u' v'] /= qj]. rewrite -!/(PathS _) in def_pi def_qj. have [x_pi' x_qj'] : x \in pi /\ x \in qj by rewrite def_pi def_qj in x_pi x_qj. have Ip : irred pi. { move: (conn_irred con_p i). by rewrite def_pi. } have Iq : irred qj. { move: (conn_irred con_q j). by rewrite def_qj. } case/(isplitP Ip) def_p : _ / x_pi' => {Ip} [p1 p2 Ip1 Ip2 Ip]. case/(isplitP Iq) def_q : _ / x_qj' => {Iq} [q1 q2 Iq1 Iq2 Iq]. case: (sep_P _ _ (pcat p1 q2)). - move: (connector_fst con_p i). by rewrite def_pi. - move: (connector_lst con_q j). by rewrite def_qj. - move => s in_P. rewrite inE. case/orP => [in_p1|in_q2]. + suff ? : s = v by subst s; rewrite [v]Ip // inE in in_P. rewrite [s](connector_right con_p (i := i)) // def_pi //. change (s \in pi). by rewrite def_p inE in_p1. + suff ? : s = u' by subst s; rewrite [u']Iq // inE in in_P. rewrite [s](connector_left con_q (i := j)) // def_qj //. change (s \in qj). by rewrite def_q inE in_q2. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)