fact: Definition nat_map_eqMix (A : eqType) := @union_map_class_eqMix nat_ordType nat_pred A _ (@natmapMixin A).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)