proposition: Lemma eq_dec (x y : t) : {eq x y} + {~ eq x y}.
proof: Proof. by rewrite /eq; case (mnmc_eq_seq x y); [left|right]. 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)