proposition: Lemma MIn_sig T (k : M.key) (m : M.t T) : M.In k m -> {e | M.MapsTo k e m}.
proof: Proof. move=> HIn. case Ee : (M.find k m) => [e|]. by exists e; apply: M.find_2. by move/F.in_find_iff in HIn. 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)