fact: Definition FPOpToFunction OP := match OP with | ADD => FPadd | SUB => FPsub | MUL => FPmul | DIV => FPdiv end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)