fact: Definition mpoly_of_effmpoly (T : ringType) n (p' : effmpoly T) : option (mpoly n T) := if P.for_all (fun k _ => size k == n)%N p' then Some [mpoly [freeg [seq (a.2, multinom_of_seqmultinom_val n a.1) | a <- M.elements p']]] else None.
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)