proposition: Lemma nth_rev n s : n < size s -> nth (rev s) n = nth s (size s - n.+1).
proof: Proof. elim/last_ind: s => // s x IHs in n *. rewrite rev_rcons size_rcons ltnS subSS -cats1 nth_cat /=. case: n => [|n] lt_n_s; first by rewrite subn0 ltnn subnn. by rewrite subnSK //= leq_subr IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)