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