proposition: Lemma smerge2_edge (u v : smerge2) : val u -- val v -> u -- v.
proof: Proof. move=> val_uv; rewrite /edge_rel/=. case: (boolP (_ && _)) => [/andP[/eqP<- _]|_]; first by rewrite sgP val_uv. case: (boolP (_ && _)) => [/andP[/eqP<- _]|_]; by rewrite val_uv. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)