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