proposition: Lemma refine_nth_def (n : nat) (m : 'X_{1..n}) (m' : seqmultinom) (i : 'I_n) x0 : refines Rseqmultinom m m' -> spec_N (nth x0 m' i) = m i.
proof: Proof. move=> rMN; move: (rMN). rewrite refinesE /Rseqmultinom /multinom_of_seqmultinom /ofun_hrel. case: sumb =>// prf [] <-. rewrite multinomE /= (tnth_nth (spec_N x0)) (nth_map x0) //. by move: prf; rewrite size_map; move/eqP ->. 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)