proposition: Lemma map2_ifft {T T' T''} (m : M.t T) (m' : M.t T') (x : M.key) (f : option T -> option T' -> option T'') : (forall t t', f (Some t) t' <> None) -> (forall t t', f t (Some t') <> None) -> M.In x (M.map2 f m m') <=> {M.In x m} + {M.In x m'}.
proof: Proof. move=> H1 H2. split; first exact: map2_2_dec. case=> HIn; apply F.in_find_iff; erewrite M.map2_1; try solve [by left|by right]; move/F.in_find_iff in HIn; by case: M.find 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)