proposition: Lemma lst_inj : injective (@lst G \o p).
proof: Proof. apply/injectiveP. apply: wlog_neg => /injectivePn [i] [j] /(conn_disjoint conn_p)/setP S /= H. move/(_ (lst (p i))) : S. by rewrite !inE H lst_mem. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)