proposition: Lemma connector_left i x : x \in p i -> x \in A -> x = fst (p i).
proof: Proof. move => in_pi in_A. move/setP : (conn_begin conn_p i) => /(_ x). rewrite !inE in_pi in_A /=. by move/esym/eqP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)