proposition: Lemma idx_swap a b x y (p : Path x y) : a \in p -> b \in p -> irred p -> a <[p] b = b <[prev p] a.
proof: Proof. move => aP bP ip. apply/idP/idP => /idx_swap_aux; auto. rewrite irred_rev prevK !mem_prev. by apply. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)