proposition: Lemma prev_inj x y : injective (@prev x y).
proof: Proof. apply: (can_inj (g := (@prev y x))) => p. exact: prevK. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)