proposition: Lemma in_fst_InA_eq_key_iff (T : Type) x s : x.1 \in [seq x.1 | x <- s] <-> InA (M.eq_key (elt:=T)) x s.
proof: Proof. split. { elim s => // h t Hind; rewrite inE; move/orP => [Hh|Ht]. { apply InA_cons_hd; change (M.eq_key _ _) with (E.eq x.1 h.1). move: Hh => /eqP ->; apply E.eq_refl. } by apply InA_cons_tl, Hind. } elim s => [|h t Hind]; [by rewrite InA_nil|]. rewrite InA_cons; elim. { change (M.eq_key _ _) with (E.eq x.1 h.1). by move/mnmc_eq_seqP/eqP =>->; rewrite inE eqxx. } by rewrite inE orb_comm; move/Hind =>->. 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)