proposition: Lemma index_rev (T : eqType) a (s : seq T) : a \in s -> uniq s -> index a (rev s) = (size s).-1 - index a s.
proof: Proof. elim: s => // b s IH. rewrite in_cons [uniq _]/=. case/predU1P => [?|A] /andP [B uniq_s]. - subst b. rewrite rev_cons index_rcons. + by rewrite eqxx index_head subn0 size_rev. + by rewrite mem_head. + by rewrite /= rev_uniq mem_rev B. - have D : b == a = false. { by apply: contraNF B => /eqP->. } rewrite rev_cons index_rcons. + rewrite eq_sym D IH //= D. by case s. + by rewrite inE mem_rev A. + by rewrite /= rev_uniq mem_rev B. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)