proposition: Lemma singleton_in_iff {T} y k (e : T) : M.In y (singleton k e) <-> E.eq k y.
proof: Proof. split; [move/F.add_in_iff|move=> H; apply/F.add_in_iff]. by intuition; move/F.empty_in_iff in H. by left. 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)