proposition: Lemma multinom_of_seqmultinom_inj n x y : size x = n -> size y = n -> multinom_of_seqmultinom n x = multinom_of_seqmultinom n y -> x = y.
proof: Proof. move=> Sx Sy; rewrite /multinom_of_seqmultinom. case (sumb _) => [prfx|] /=; [|by rewrite size_map Sx eqxx]. case (sumb _) => [prfy|] /=; [|by rewrite size_map Sy eqxx]. case; exact: map_spec_N_inj. 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)