proposition: Lemma refine_seqmultinomP (n : nat) (m : 'X_{1..n}) (m' : seqmultinom) : size m' = n -> (forall i : 'I_n, spec_N (nth 0%num m' i) = m i) -> refines Rseqmultinom m m'.
proof: Proof. move=> eq_sz eq_nth. rewrite refinesE /Rseqmultinom /multinom_of_seqmultinom /ofun_hrel. case: sumb => [prf|]. congr Some; apply: val_inj; simpl. apply: eq_from_tnth => i. rewrite (tnth_nth 0%N) /= (nth_map 0%num) ?eq_nth //. by move: prf; rewrite size_map; move/eqP ->. by rewrite size_map eq_sz eqxx. 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)