fact: Definition binary_fun_R (f : Expr_BinaryOp) : R->R->R := match f with | EB_Add => Rplus | EB_Sub => Rminus | EB_Mul => Rmult | EB_Div => Rdiv | EB_Max => Rmax | EB_Min => Rmin end.
imports: Reals ZArith QArith Lra Lia Ltac2.Ltac2 Ltac2.Printf Ltac2.Bool