proposition: Lemma next_map (aT rT : eqType) (f : aT -> rT) (s : seq aT) (x : aT) : injective f -> next (map f s) (f x) = f (next s x).
proof: Proof. move=> inj_f; case: s => //= a s. by elim: s a {2 4}a => /= [|y s IHs] a b; rewrite inj_eq // ?IHs -fun_if. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)