proposition: Lemma refine_seq_multinom_coeff n (s : seq ('X_{1..n} * T)) s' : all (fun mc => size mc.1 == n) s' -> s = [seq (multinom_of_seqmultinom_val n mc.1, mc.2) |mc <- s'] -> refines (list_R (prod_R Rseqmultinom eq)) s s'.
proof: Proof. rewrite refinesE. elim: s' s=> [|h' t' IH]; case=> [//|h t] //=. case/andP => Hsh Hst [Hh Ht]; constructor. { apply/prod_RI; rewrite Hh; split=>//. by apply refinesP; eapply refine_multinom_of_seqmultinom_val. } by apply IH. 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)