proposition: Lemma connector_lst i : lst (p i) \in B.
proof: Proof. move/setP : (conn_end conn_p i) => /(_ (lst (p i))). rewrite !inE eqxx. by case/andP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)