proposition: Lemma refine_size_mpoly (n : nat) T (p : mpoly n T) (p' : effmpoly T) `{ref_pp' : !refines Reffmpoly p p'} : forall m, M.In m p' -> size m == n.
proof: Proof. move: ref_pp'. rewrite refinesE /Reffmpoly /mpoly_of_effmpoly /ofun_hrel. set t := P.for_all _ _; case_eq t => //. rewrite /t (P.for_all_iff _); [|by move=> m _ /mnmc_eq_seqP /eqP <-]. by move=> H _ m [e Hme]; apply (H m e). 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)