proposition: Lemma smerge2_sym : symmetric smerge2_rel.
proof: Proof. move => u v /=; (case: (altP (sval u =P x)); case: (altP (sval v =P x)) => //=) => [-> -> //|]. by rewrite sgP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)