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