proposition: Lemma connector_extend A B n (p : 'I_n -> pathS G) x y i : x \notin \bigcup_i [set z in p i] -> fst (p i) = y -> x -- y -> x \notin B -> connector A B p -> exists q : 'I_n -> pathS G, connector (x |: (A :\ y)) B q.
proof: Proof. move => Hx Hy xy xB conn_p. have xDy : x != y. { apply: contraNneq Hx => ->. apply/bigcupP; exists i => //. by rewrite inE -Hy fst_mem. } set A' := _ |: _. pose q (j : 'I_n) := if j == i then pcatS (PathS (edgep xy)) (p j) else p j. have Hj (j : 'I_n) u : j != i -> u \in tagged (p j) -> (u == y = false)*(u == x = false). { move => jDi u_pi. split. - apply: contra_eqF (conn_disjoint conn_p jDi) => /eqP ?; subst. apply/set0Pn; exists (fst (p i)). by rewrite !inE u_pi. - apply: contraNF Hx => /eqP <-. apply/bigcupP; exists j => //. by rewrite inE. } exists q. split. - move => j. rewrite /q /=. case: (altP (j =P i)) => [E|D]; last exact: (conn_irred conn_p). subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /= irred_edgeL. rewrite (conn_irred conn_p) andbT. apply: contraNN Hx => Hx. apply/bigcupP. exists i => //. by rewrite inE. - move => j. rewrite /q. case: (altP (j =P i)) => [E|D]. + subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /=. apply/setP => u. rewrite [A']lock !inE -lock. apply/andP/idP. * rewrite !inE mem_edgep /=. case: (altP (u =P x)) => [-> //|/=]. rewrite -/(fst (p i)). case: (altP (u =P fst (p i))) => [_ _ [_ ?] //|]. rewrite /= -/(fst (p i)) => [H1 H2 [H3 H4]]. by rewrite -(connector_left conn_p _ H4) ?eqxx in H1. * move/eqP->. by rewrite mem_edgep /= !inE eqxx. + rewrite -(conn_begin conn_p). apply/setP => u. rewrite !inE. case e: (u \in _) => //=. by rewrite !(Hj j) /=. - move => j. rewrite /q. case: (altP (j =P i)) => [E|D]; last exact: (conn_end conn_p). subst j. rewrite [p i]pathS_eta. subst y. rewrite pcatSE /= -/(lst _). apply/setP => u. rewrite -(conn_end conn_p i) !inE -mem_pcat. case uB : (u \in B) => //. rewrite !andbT. apply/edgeLP/idP => /=; last by right. case => [?|//]. subst. by rewrite uB in xB. - move => j1 j2. rewrite /q. have jP j : i != j -> [set x0 in pcatS (PathS (edgep xy)) (p i)] :&: [set x0 in p j] = set0. { move => jDi. rewrite [p i]pathS_eta. subst y. rewrite pcatSE. apply: contra_eq (conn_disjoint conn_p jDi). case/set0Pn => u /setIP []. rewrite 2!inE /=. case/edgeLP => /= [-> Hx'|Hu ?]. * apply: contraNN Hx => _. apply/bigcupP; exists j => //. by rewrite inE. * apply/set0Pn. exists u. by rewrite !inE Hu. } case: (altP (j1 =P i)); case: (altP (j2 =P i)). + move => -> -> . by rewrite eqxx. + rewrite eq_sym => Hj2 ->. exact: jP. + rewrite eq_sym setIC. move => -> Hj2 _. exact: jP. + move => _ _. exact: (conn_disjoint conn_p). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)