proposition: Lemma refine_seqmultinom_of_multinom (n : nat) (m : 'X_{1..n}) : refines Rseqmultinom m (seqmultinom_of_multinom m).
proof: Proof. by rewrite refinesE /Rseqmultinom /ofun_hrel seqmultinom_of_multinomK. 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)