proposition: Lemma NoDupA_eq_key_uniq_fst elt s : NoDupA (M.eq_key (elt:=elt)) s -> uniq [seq i.1 | i <- s].
proof: Proof. elim s => // h t Hind Hnd /=. inversion Hnd as [x|h' t' H1 H2]. apply/andP; split; [|by apply Hind]. by apply/negP => Hin; apply H1, in_fst_InA_eq_key_iff. 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)