proposition: Lemma map_mapsto_iff_dec {T T'} (m : M.t T) (x : M.key) (b : T') (f : T -> T') : M.MapsTo x b (M.map f m) <=> {a : T | b = f a /\ M.MapsTo x a m}.
proof: Proof. split. case_eq (M.find x m) => [e He|] H. exists e. split. apply (F.MapsTo_fun (m:=M.map f m) (x:=x)); auto. apply M.find_2. by rewrite F.map_o /option_map He. by apply M.find_2. move=> H0. have H1 : (M.In x (M.map f m)) by exists b; auto. have [a H2] := MIn_sig (M.map_2 H1). rewrite (M.find_1 H2) in H; discriminate. intros (a,(H,H0)). subst b. exact: M.map_1. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)