proposition: Lemma index_rcons (T : eqType) a b (s : seq T): a \in b::s -> uniq (b :: s) -> index a (rcons s b) = if a == b then size s else index a s.
proof: Proof. case: (boolP (a == b)) => [/eqP<- _|]. - elim: s a {b} => //= [|b s IH] a; first by rewrite eqxx. rewrite !inE negb_or -andbA => /and4P[A B C D]. rewrite eq_sym (negbTE A) IH //. - elim: s a b => //. + move => a b. by rewrite inE => /negbTE->. + move => c s IH a b A. rewrite inE (negbTE A) /=. rewrite inE eq_sym. case: (boolP (c == a)) => //= B C D. rewrite IH //. * by rewrite inE C. * case/and3P:D => D1 D2 D3. rewrite /= D3 andbT. apply: contraNN D1; exact: mem_tail. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)