proposition: Lemma prev_irred x y (p : Path x y) : irred p -> irred (prev p).
proof: Proof. rewrite /irred /nodes => U. apply: leq_size_uniq U _ _. - move => u. by rewrite mem_prev. - by rewrite -!lock /= ltnS /srev size_rev size_belast. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)