fact: Definition multinom_of_seqmultinom_val n (m : seqmultinom) : 'X_{1..n} := odflt (@mnm0 n) (multinom_of_seqmultinom n m).
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)