proposition: Lemma refine_nth (n : nat) (m : 'X_{1..n}) (m' : seqmultinom) (i : 'I_n) : refines Rseqmultinom m m' -> spec_N (nth 0%num m' i) = m i.
proof: Proof. exact: refine_nth_def. 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)