fact: Definition mpoly_add_eff : effmpoly T -> effmpoly T -> effmpoly T := M.map2 (fun c1 c2 => match c1, c2 with | Some c1, Some c2 => Some (c1 + c2)%C | Some c, _ | _, Some c => Some c | None, None => None end).
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)