proposition: Lemma not_In_mcoeff {n} m m' p p' : refines (Reffmpoly (T := T) (n := n)) p p' -> refines Rseqmultinom m m' -> ~ M.In m' p' -> p@_m = 0.
proof: Proof. move=> Hp Hm Hin; rewrite (refine_find_mpoly Hp Hm). by move/F.not_find_in_iff: 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)