proposition: Lemma connector_right i x : x \in p i -> x \in B -> x = lst (p i).
proof: Proof. move => in_pi in_B. move/setP : (conn_end conn_p i) => /(_ x). rewrite !inE in_pi in_B /=. by move/esym/eqP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)