fact: Definition mpoly_sub_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 => Some (- c)%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)