fact: Definition eq_ereal (x y : \bar R) := match x, y with | x%:E, y%:E => x == y | +oo, +oo => true | -oo, -oo => true | _, _ => false end.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed