proposition: Lemma link_rel_sep2 (G : sgraph) (x y : G) : connected [set: G] -> ~~ x -- y -> link_rel x y -> x != y /\ forall S, separates x y S -> 2 <= #|S|.
proof: Proof. move => con_G xNy /andP [xDy cp_sub]. split => // S sep_xy. case E : #|S| => [|[|//]]. - move/cards0_eq : E => E. subst S. move/connectedTE : con_G => /(_ x y). apply: contraTT => _. exact/separates0P. - move/eqP/cards1P : E => [z Hz]. subst. move/sepatates_cp in sep_xy. by set_tac. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)