proposition: Lemma smerge2_minor : x -- y -> minor G smerge2.
proof: Proof. move => xy. pose phi (z : smerge2) : {set G} := if val z == x then [set x;y] else [set val z]. suff: minor_rmap phi by apply: minor_of_rmap. split. - move => z; rewrite /phi; case: ifP => _; solve [exact: set10|exact: setU1_neq]. - move => z; rewrite /phi; case: ifP => _; solve [exact: connected1|exact: connected2]. - move => z1 z2 z1Dz2; rewrite /phi. case: (eqVneq x (val z1)) => [->|xDz1]. + rewrite eq_sym val_eqE (negbTE z1Dz2) disjoint_sym disjoints1 !inE negb_or. by rewrite eq_sym val_eqE (negbTE z1Dz2) (valP z2). + case: (eqVneq x (val z2)) => [->|xDz2]; rewrite disjoints1 !inE ?negb_or ?val_eqE //. by rewrite z1Dz2 (valP z1). - have H z u v : sval u = x -> sval v != x -> sval v -- z -> z \in [set x; y] -> neighbor (phi u) (phi v). { move => eq_u eq_v v_z Hz. apply/neighborP; exists z; exists (sval v). by rewrite /phi [val u]eq_u eqxx (negbTE eq_v) sgP v_z Hz inE eqxx. } move => u v. rewrite /edge_rel/=. case: (altP (sval u =P x)); case: (altP (sval v =P x)) => //=. + move => -> ->. by rewrite sgP. + move => eq_v eq_u. by case/orP => ?; [apply: (H x)|apply: (H y)]; rewrite //= !inE !eqxx. + move => eq_v eq_u. rewrite neighborC. by case/orP => ?; [apply: (H x)|apply: (H y)]; rewrite //= !inE !eqxx. + move => eq_v eq_u u_v. apply/neighborP; exists (val u); exists (val v). by rewrite /phi /= (negbTE eq_v) (negbTE eq_u) 2!sgP !inE !eqxx u_v. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)