fact: Definition ROpToFunction OP := match OP with | ADD => Rplus | SUB => Rminus | MUL => Rmult | DIV => Rdiv end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)