proposition: Lemma map_preim (s : seq T') : {subset s <= codom f} -> map f (preim_seq s) = s.
proof: Proof. elim: s => //= y s IHs; case: pickP => [x /eqP fx_y | nfTy] fTs. by rewrite /= fx_y IHs // => z s_z; apply: fTs; apply: predU1r. by case/imageP: (fTs y (mem_head y s)) => x _ fx_y; case/eqP: (nfTy x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)