proposition: Lemma prev_map p : uniq p -> forall x, prev (map h p) (h x) = h (prev p x).
proof: Proof. move=> Up x; rewrite -[x in LHS](next_prev Up) -(next_map Up). by rewrite prev_next ?map_inj_uniq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)