proposition: Lemma connectorC_edge (G : diGraph) (A : {set G}) n (p : 'I_n -> pathS G) i : connector A (~: A) p -> exists fl : fst (p i) -- lst (p i), p i = PathS (edgep fl).
proof: Proof. move => conn_p. case def_q : (p i) => [[a b] /= q]. rewrite -/(PathS q) in def_q *. case: (irred_is_edge q). - move: (conn_irred conn_p i). by rewrite def_q. - case: (altP (a =P b)) => // ?; subst. move: (connector_fst conn_p i) (connector_lst conn_p i). by rewrite def_q !inE => ->. - move => z zq. rewrite !inE. case: (boolP (z \in A)) => [zA|zNA]. + by rewrite [z](connector_left conn_p (i := i)) ?def_q // eqxx. + by rewrite {2}[z](connector_right conn_p (i := i)) ?def_q ?inE // eqxx. - move => ab ->. by exists ab. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)