proposition: Lemma fst_lst_eq i j : fst (p i) = lst (p j) -> i = j.
proof: Proof. move => E. apply: (connector_eq (x := fst (p i))); first exact: fst_mem. by rewrite E lst_mem. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)