proposition: Lemma in_InA_eq_key_elt_iff (T : eqType) x s : x \in s <-> InA (M.eq_key_elt (elt:=T)) x s.
proof: Proof. split. { elim s => // h t Hind; rewrite inE; move/orP => [Hh|Ht]. { by move: Hh => /eqP ->; apply InA_cons_hd; split; [apply E.eq_refl|]. } by apply InA_cons_tl, Hind. } elim s => [|h t Hind]; [by rewrite InA_nil|]. rewrite InA_cons; elim. { by move/eq_key_elt_eq=>->; rewrite inE eqxx. } by move/Hind; rewrite inE orb_comm=>->. 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)