fact: Definition PFOpToFunction OP := match OP with | ADD => PrimFloat.add | SUB => PrimFloat.sub | MUL => PrimFloat.mul | DIV => PrimFloat.div end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)