proposition: Lemma minor_rmap_comp (G H K : sgraph) (f : H -> {set G}) (g : K -> {set H}) : minor_rmap f -> minor_rmap g -> minor_rmap (fun x => \bigcup_(y in g x) f y).
proof: Proof. move => [f1 f2 f3 f4] [g1 g2 g3 g4]. split => [x|x|x1 x2|x1 x2]. - case/set0Pn: (g1 x) => y Gy; case/set0Pn: (f1 y) => z Fz. by apply/set0Pn; exists z; apply/bigcupP; exists y. - move => z1 z2 /bigcupP [y1 y1_g z1_f] /bigcupP [y2 y2_g z2_f]. have/connectP [p] := (g2 _ _ _ y1_g y2_g). elim: p z1 y1 y1_g z1_f => /= [|y1' p IHp] z1 y1 y1_g z1_f. + move => _ ?; subst. apply: connect_restrict_mono; [exact: bigcup_sup y1_g|exact: f2]. + rewrite -andbA => /and3P [/andP [H1 H2] H3 H4 H5]. case/neighborP: (f4 _ _ H3) => a [b] [a_fy1 b_fy1' ab]. apply: connect_trans (IHp _ _ H2 b_fy1' H4 H5). apply: (@connect_trans _ _ a). * apply: connect_restrict_mono. apply: bigcup_sup y1_g. exact: f2. * apply: connect1 => /=. by rewrite ab andbT (mem_bigcup y1) ?(mem_bigcup y1'). - move/g3 => Dx. apply/disjointP => z. case/bigcupP => y1 y1_g z_fy1; case/bigcupP => y2 y2_g z_fy2. suff: y1 != y2 by move/f3/disjointP/(_ z); apply. apply: contraTneq y2_g => <-. by rewrite (disjointFr Dx). - move/g4/neighborP => [y1] [y2] [Y1 Y2 /f4 /neighborP [z1] [z2] [? ? e]]. by apply/neighborP; exists z1; exists z2; rewrite (mem_bigcup y1) ?(mem_bigcup y2). Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)