proposition: Lemma refine_size (n : nat) (m : 'X_{1..n}) (m' : seqmultinom) `{ref_mm' : !refines Rseqmultinom m m'} : size m' = n.
proof: Proof. move: ref_mm'. rewrite refinesE /Rseqmultinom /multinom_of_seqmultinom /ofun_hrel. case: sumb =>// prf _. rewrite size_map in prf. exact/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)