fact: Definition M2R {T} : evalExprTypeRounded T -> R := match T with | Integer => fun x => IZR x | BinFloat => fun x => x end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)