proposition: Lemma MIn_dec {T} k (m : M.t T) : decidable (M.In k m).
proof: Proof. case E: (M.mem k m); [left|right]; apply/F.mem_in_iff =>//. by rewrite E. 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)