proposition: Lemma smerge_konnected k (G : sgraph) (x y : G) : x -- y -> k.+1.-connected G -> k.-connected (smerge2 G x y).
proof: Proof. move=> xy [lG vsG]; split => [|S sepS]; first by rewrite -ltnS card_smerge2. have/vsG := smerge2_separator sepS. rewrite cardsU1 card_imset // [_ \notin _](_ : _ = true) //. by apply: contraTN isT => /imsetP -[[z zDy _ /= E]]; rewrite -E eqxx in zDy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)