proposition: Lemma unused_rmap_add_edge_r (M : sgraph) (phi : M -> {set G'}) : (forall i, y \notin phi i) -> minor_rmap phi -> @minor_rmap G M phi.
proof: Proof. move => y_unused [P1 P2 P3 P4]. have Y u i : u \in phi i -> u == y = false by apply: contraTF => /eqP ->. split => //; last by move => i j ij; apply: neighbor_del_edge2 (P4 i j ij). move => i u v u_pi v_pi; have:= P2 i u v u_pi v_pi. exact/connect_mono/unused_add_edge_connect_r/y_unused. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)