proposition: Lemma card_smerge2 (G : sgraph) (x y : G) : #|smerge2 G x y|.+1 = #|G|.
proof: Proof. rewrite card_sig [RHS](cardD1 y) add1n; congr (_.+1). by apply: eq_card => z; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)