proposition: Lemma add_edge_break (G : sgraph) (s1 s2 x y : G) (p : @Path (add_edge s1 s2) x y) : s1 != s2 -> let U := [set s1;s2] in irred p -> ~~ @connect G sedge x y -> exists u v : G, exists q1 : Path x u, exists q2 : Path v y, [/\ u \in U, v \in U, u != v & nodes p = nodes q1 ++ nodes q2].
proof: Proof. move => D U Ip NCxy. have/andP [H1 H2] : (s1 \in p) && (s2 \in p). { rewrite -[_ && _]negbK negb_and. apply: contraNN NCxy => H. case: (add_edge_avoid p H) => p' Ep. exact: Path_connect. } case: (@split_at_first (add_edge s1 s2) (mem U) _ _ p s1) => //. { by rewrite !inE eqxx. } move => z [p1] [p2] [P1 P2 P3]. subst U. wlog ? : s1 s2 p D Ip NCxy H1 H2 z p1 p2 P1 P3 {P2 H1} / z = s1. { move => W. case/setUP : P2 => /set1P P2; subst z. - by apply W with s1 p1 p2. - case: (add_edge_pathC p) => p' Ep. case: (add_edge_pathC p1) => p1' Ep1. case: (add_edge_pathC p2) => p2' Ep2. pose G':= add_edge s1 s2. pose G'' := add_edge s2 s1. case: (W s2 s1 p' _ _ _ _ _ s2 p1' p2') => //. + by rewrite eq_sym. + by rewrite irredE Ep. + by rewrite (@mem_path G'') Ep -(@mem_path G'). + by rewrite (@mem_path G'') Ep -(@mem_path G'). + apply/eqP. by rewrite -nodes_eqE Ep P1 !nodes_pcat Ep1 Ep2. + move => z. rewrite setUC. rewrite (@mem_path G'') Ep1 -(@mem_path G'). exact: P3. + move => u [v] [q1] [q2]. rewrite setUC => [[? ? ? E]]. exists u. exists v. exists q1. exists q2. split => //. congruence. } subst. move: H2. rewrite (@mem_pcat (add_edge s1 s2)). have {P3} s2p1 : s2 \notin p1. apply: contraNN D => C. by rewrite [s2]P3 ?inE ?eqxx. rewrite (negbTE s2p1) /= => s2p2. case/irred_catE : Ip => Ip1 Ip2 Ip12. case: (splitL p2) => [|z [s1z] [pR [def_p2 _]]]. { apply: contraNneq D => ?;subst y. move: s2p2. by rewrite [p2]irredxx // mem_idp eq_sym. } move: Ip2. rewrite def_p2 irred_edgeL => /andP [s1pR IpR]. case: (add_edge_avoid p1) => [|p1' Ep]; first by rewrite s2p1. case: (add_edge_avoid pR) => [|pR' ER]; first by rewrite s1pR. have ? : z = s2. { apply: contraNeq NCxy => zNs2. move: (s1z) => /=. rewrite /edge_rel/= (negbTE zNs2) [z == s1]eq_sym (sg_edgeNeq s1z) ?eqxx. case/or3P => //= s1z'. exact: (Path_connect (pcat p1' (pcat (edgep s1z') pR'))). } subst z. exists s1; exists s2; exists p1'; exists pR'. rewrite !inE ?eqxx. split => //. rewrite Ep ER. by rewrite !nodesE. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)