proposition: Lemma minor_induced_add_node (G : sgraph) (N : {set G}) : @minor_map (induced [set~ None : add_node G N]) G val.
proof: Proof. have inNoneD (a : G) : Some a \in [set~ None] by rewrite !inE. split. + move=> y. by exists (Sub (Some y) (inNoneD y)). + move=> y x1 x2. rewrite -!mem_preim =>/eqP<- /eqP/val_inj->. exact: connect0. + move=> x y xy. exists (Sub (Some x) (inNoneD x)). exists (Sub (Some y) (inNoneD y)). by split; rewrite -?mem_preim. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)