proposition: Lemma singleton_mapsto {T} k k' (e e' : T) : M.MapsTo k e (singleton k' e') -> (k = k' /\ e = e').
proof: Proof. rewrite F.add_mapsto_iff; elim; move=> [Hk He]; [split; [|by[]]|]. by move/mnmc_eq_seqP/eqP in Hk. by move: He; rewrite F.empty_mapsto_iff. 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)