proposition: Lemma MapsTo_mcoeff {n} m m' p p' a : refines (Reffmpoly (T := T) (n := n)) p p' -> refines Rseqmultinom m m' -> M.MapsTo m' a p' -> p@_m = a.
proof: Proof. move=> Hp Hm HMT; move/F.find_mapsto_iff in HMT. by rewrite (refine_find_mpoly Hp Hm) /odflt /oapp HMT. 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)