fact: Definition multinom_of_seqmultinom n (m : seqmultinom) : option 'X_{1..n} := let m' := map spec_N m in if sumb (size m' == n) is left prf then Some (Multinom (@Tuple n nat m' prf)) 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)