proposition: Lemma rmap_add_edge_sym (G H : sgraph) (s1 s2 : G) (phi : H -> {set G}) : @minor_rmap (add_edge s1 s2) H phi -> @minor_rmap (add_edge s2 s1) H phi.
proof: Proof. case => [P1 P2 P3 P4]; split => //. - move => x. exact/add_edge_connected_sym. - move => x y /P4/neighborP => [[x'] [y'] [A B C]]. apply/neighborP; exists x'; exists y'. by rewrite add_edgeC. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)