proposition: Lemma seqmultinom_of_multinomK n : pcancel (@seqmultinom_of_multinom n) (@multinom_of_seqmultinom n).
proof: Proof. move=> x; rewrite /seqmultinom_of_multinom /multinom_of_seqmultinom. case: sumb => [prf|]. congr Some; apply: val_inj; simpl; apply: val_inj; simpl; case: (x). by move=> t; rewrite -map_comp (eq_map implem_NK) map_id. case: x => [t]. by rewrite size_tuple 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)