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