proposition: Lemma unused_add_edge_connect_r (A : {pred G}) : y \notin A -> subrel (restrict A (@sedge G')) (restrict A (@sedge G)).
proof: Proof. move=> yNA u v /=; rewrite -!andbA => /and3P [uA vA]. gen have H,-> : u uA / u == y = false; first by apply:contraTF uA => /eqP->. by rewrite (H v) // !andbF !orbF uA vA. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)