proposition: Lemma prev_rev p : uniq p -> prev (rev p) =1 next p.
proof: Proof. move=> Up x; case p_x: (x \in p); last first. by rewrite next_nth prev_nth mem_rev p_x. case/rot_to: p_x (Up) => [i q def_p] Urp; rewrite -rev_uniq in Urp. rewrite -(prev_rotr i Urp); do 2 rewrite -(prev_rotr 1) ?rotr_uniq //. rewrite -rev_rot -(next_rot i Up) {i p Up Urp}def_p. by case: q => // y q; rewrite !rev_cons !(=^~ rcons_cons, rotr1_rcons) /= eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)