fact: Definition round_nearest_even mx lx := match lx with | loc_Exact => mx | loc_Inexact Lt => mx | loc_Inexact Eq => if Z.even mx then mx else (mx + 1)%Z | loc_Inexact Gt => (mx + 1)%Z end.
imports: ZArith FloatClass