proposition: Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
proof: Proof. by move=> x y z /mnmc_eq_seqP/eqP =>->. 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)