proposition: Lemma refine_mnm0 n : refines Rseqmultinom (@mnm0 n) (@mnm0_seq n).
proof: Proof. apply refine_seqmultinomP. by rewrite size_nseq. move=> i; rewrite nth_nseq if_same multinomE (tnth_nth 0%N) nth_map //=. by rewrite size_enum_ord. 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)