proposition: Lemma eq_key_elt_eq T x y : (M.eq_key_elt (elt:=T)) x y <-> x = y.
proof: Proof. split. { move=> [H1 H2]. rewrite (surjective_pairing x) (surjective_pairing y); f_equal=> //. by apply/eqP/mnmc_eq_seqP. } move=> ->; split=> //; apply E.eq_refl. 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)