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