proposition: Lemma idx_swap_aux a b x y (p : Path x y) : a \in p -> b \in p -> irred p -> idx p a < idx p b -> idx (prev p) b < idx (prev p) a.
proof: Proof. move => aP bP ip A. rewrite !idx_srev //. apply: ltn_sub2l => //. apply: (@leq_trans (idx p b)) => //. rewrite -ltnS -[X in _ < X]/(size (x :: pval p)). by rewrite -nodesE index_mem. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)