fact: Definition ArithOpToCArithOp T OP := match OP with | ADD => CADD | SUB => CSUB | MUL => CMUL | DIV => match T with | Integer => CINTDIV | BinFloat => CFLTDIV end end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr