fact: Definition M_hrel (m : M.t A) (m' : M.t C) : Type := ((forall k, M.In k m <-> M.In k m') * forall k e e', M.MapsTo k e m -> M.MapsTo k e' m' -> rAC e e')%type.
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)