fact: Definition er_map T T' (f : T -> T') (x : \bar T) : \bar T' := match x with | r%:E => (f r)%:E | +oo => +oo | -oo => -oo end.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed