proposition: Lemma Rseqmultinom_eq n (x : 'X_{1..n}) x' y y' : refines Rseqmultinom x x' -> refines Rseqmultinom y y' -> (x == y) = (x' == y').
proof: Proof. move=> Hx Hy; apply/idP/idP => H. { have Sx' := @refine_size _ _ _ Hx. have Sy' := @refine_size _ _ _ Hy. apply/eqP. move: H Hy Hx; rewrite refinesE /Rseqmultinom /ofun_hrel; move/eqP=>-><-. by apply multinom_of_seqmultinom_inj. } apply/eqP; move: H Hx Hy. rewrite refinesE /Rseqmultinom /ofun_hrel; move/eqP=>->->. by move=> H; inversion H. 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)