proposition: Lemma in_InA_iff mc l : mc \in l <-> InA (M.eq_key_elt (elt:=T)) mc l.
proof: Proof. elim l=> [|h t IH]; [by split=>// H; inversion H|]. rewrite in_cons; split. { move=>/orP []; [by move/eqP->; left; rewrite eq_key_elt_eq|]. by move=> Hmc; right; apply IH. } move=> H; inversion H as [mc' l' Hmc [Hmc' Hl']|mc' l' Hmc [Hmc' Hl']]. { by apply/orP; left; apply/eqP; apply eq_key_elt_eq. } by apply/orP; right; rewrite IH. 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)