proposition: Lemma add_mapsto_iff_dec {T} (m : M.t T) (x y : M.key) (e e' : T) : (M.MapsTo y e' (M.add x e m) <=> {(E.eq x y) * (e = e')} + {(~ E.eq x y) * (M.MapsTo y e' m)})%type.
proof: Proof. split. destruct (E.eq_dec x y); [left|right]. split; auto. symmetry; apply (F.MapsTo_fun (e':=e) H). exact: M.add_1. split; auto; apply M.add_3 with x e; auto. case; case => H1 H2. - rewrite H2; exact: M.add_1. - exact: M.add_2. 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)