proposition: Lemma refine_multinom_of_seqmultinom_val (n : nat) (m : seqmultinom) : size m == n -> refines Rseqmultinom (multinom_of_seqmultinom_val n m) m.
proof: Proof. move=> Hsz. rewrite refinesE /Rseqmultinom /multinom_of_seqmultinom_val /ofun_hrel. case_eq (multinom_of_seqmultinom n m) => //. rewrite /multinom_of_seqmultinom; case sumb => //. by rewrite size_map Hsz. 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)