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