proposition: Lemma ssplit_K4_nontrivial (G : sgraph) (i o : G) : ~~ i -- o -> link_rel i o -> K4_free (add_edge G i o) -> connected [set: G] -> disconnected (sinterval i o).
proof: Proof. move => io1 L K4F conn_G. case: (link_rel_sep2 conn_G io1 L) => io2 io3 {L}. case: (theta io1 io2 io3) => p indep_p. case: (theta_vertices p io2 io1) => x in_p. apply/disconnectedE => conn_io. have in_io j : x j \in sinterval i o. { apply: irred_in_sinterval (in_p _). exact: valP. } case: (path_in_connected conn_io (in_io ord0) (in_io ord1)) => q' Iq /subsetP sub_io. case: (split_at_first (A := mem (interior (p ord1))) (p := q') (k := x ord1)). all: try by [exact: in_p|]. move => x2 [q1'] [q2] [E Q1 Q2]. have Iq1 : irred q1'. move: Iq. rewrite E. by case/irred_catE. apply: K4F. case: (add_edge_Path i o (p ord0)) => p0 N0. case: (add_edge_Path i o (p ord1)) => p1 N1. case: (add_edge_Path i o q1') => q Nq. have io : i -- o :> add_edge G i o by rewrite /edge_rel/= io2 !eqxx. pose p2 := edgep io. apply (@K4_of_paths (add_edge G i o)) with i o (x ord0) x2 p0 p1 p2 q => //. - rewrite (independent_nodes N0 N1). exact: indep_p. - by rewrite /independent interior_edgep disjoint_sym eq_disjoint0. - by rewrite /independent interior_edgep disjoint_sym eq_disjoint0. - by rewrite (interior_eq_nodes N0). - by rewrite (interior_eq_nodes N1). - rewrite (irred_eq_nodes N0). exact: valP. - rewrite (irred_eq_nodes N1). exact: valP. - exact: irred_edge. - by rewrite (irred_eq_nodes Nq). - apply/disjointP => z. rewrite (mem_eq_nodes Nq) => z_q1'. case/set2P => [?|?]; subst. + move: (sub_io i). by rewrite sinterval_bounds !inE z_q1' => /(_ isT). + move: (sub_io o). by rewrite sinterval_bounds !inE z_q1' => /(_ isT). - move => z. rewrite (interior_edgep) inE /= in_set0 orbF (mem_eq_nodes Nq). rewrite (interior_eq_nodes N1). exact: Q2. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)