proposition: Lemma add_node_minor (G G' : sgraph) (U : {set G}) (U' : {set G'}) (phi : G -> G') : (forall y, y \in U' -> exists2 x, x \in U & phi x = y) -> total_minor_map phi -> minor (add_node G U) (add_node G' U').
proof: Proof. move => H [M1 M2 M3]. apply: strict_is_minor. exists (omap phi). split. - case => [y|]; last by exists None. case: (M1 y) => x E. exists (Some x). by rewrite /= E. - move => [y|]. + rewrite preim_omap_Some. exact: connected_add_node. + rewrite preim_omap_None. exact: connected1. - move => [x|] [y|] //=. + move/M3 => [x0] [y0] [H1 H2 H3]. exists (Some x0); exists (Some y0). by rewrite !preim_omap_Some !imset_f. + move/H => [x0] H1 H2. exists (Some x0); exists None. rewrite !preim_omap_Some !preim_omap_None !inE !eqxx !imset_f //. by rewrite -mem_preim H2. + move/H => [y0] H1 H2. exists None; exists (Some y0). rewrite !preim_omap_Some !preim_omap_None !inE !eqxx !imset_f //. by rewrite -mem_preim H2. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)