proposition: Lemma map2_2_dec {T T' T''} (m : M.t T) (m' : M.t T') (x : M.key) (f : option T -> option T' -> option T'') : M.In x (M.map2 f m m') -> {M.In x m} + {M.In x m'}.
proof: Proof. move=> HIn; apply: or_dec; try exact: MIn_dec. exact: M.map2_2 HIn. 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)