proposition: Lemma sdecomp_sskel (T : forest) (G : graph2) (B : T -> {set G}) : sdecomp T (sskeleton G) B <-> (sdecomp T G B /\ compatible B).
proof: Proof. split. - case => [D1 D2 D3]. split. split => //. + move => x y /= xy. apply: D2. by rewrite /edge_rel/= xy. + case: (altP (input =P output :> skeleton G)) => E. * case: (D1 input) => t Ht. exists t. by rewrite -E !Ht. * suff: (input : sskeleton G) -- output by apply: D2. by rewrite /edge_rel/= E !eqxx. - move => [[D1 D2 D3] C]. split => //= x y. case/or3P; first exact: D2. + case/and3P => ? /eqP E1 /eqP E2. by subst. + case/and3P => ? /eqP E1 /eqP E2. subst. case: C => t. rewrite andbC. by exists t. Qed.
imports: Coq(RelationClasses Setoid) mathcomp(all_ssreflect) GraphTheory(edone set_tac finite_quotient preliminaries) GraphTheory(digraph sgraph treewidth minor equiv setoid_bigop) GraphTheory(structures mgraph pttdom ptt mgraph2 skeleton)