proposition: Lemma RseqmultinomE {n} m m' : refines (Rseqmultinom (n := n)) m m' <=> m = map spec_N m' :> seq nat.
proof: Proof. split => Hmain. { apply eq_from_nth with (x0 := O). { by rewrite size_map size_tuple (@refine_size _ m). } move=> i Hi. rewrite size_tuple in Hi. case: n m Hmain Hi => // n m Hmain Hi. rewrite -(inordK Hi) (nth_map 0%num); last by rewrite (@refine_size _ m). by rewrite (@refine_nth _ m) -tnth_nth. } have Hsz : size m' = size m by rewrite Hmain size_map. apply: refine_seqmultinomP. { by rewrite Hsz size_tuple. } case: n m Hmain Hsz => [|n] m Hmain Hsz; first by case. by move=> i; rewrite (mnm_nth O) Hmain (nth_map 0%num 0%N) // Hsz size_tuple. 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)