proposition: Lemma decomp_link (G : sgraph) (D : T -> {set G}) (A : {set G}) : A \subset \bigcup_(t in U) D t -> sdecomp T G D -> @sdecomp tlink G (decompL D A).
proof: Proof. move => HA decD. split => //. - move => x. case: (sbag_cover decD x) => t Ht. by exists (Some t). - move => x y xy. case: (sbag_edge decD xy) => t Ht. by exists (Some t). - have X x a : x \in D a -> x \in A -> connect (restrict [pred t | x \in decompL D A t] (add_node_rel U)) (Some a) None. { move => H1 H2. move/(subsetP HA) : (H2) => /bigcupP [t Ht1 Ht2]. apply: (connect_trans (y := Some t)). - move: (sbag_conn decD H1 Ht2). exact: homo_connect. - apply: connect1 => /=; by rewrite !in_simpl H2 Ht1. } move => x [a|] [b|] /= H1 H2; last exact: connect0. + move: (sbag_conn decD H1 H2). exact: homo_connect. + exact: X. + rewrite (@srestrict_sym link). exact: X. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)