diff --git a/src/arith/sidekick_arith.ml b/src/arith/sidekick_arith.ml
index a6c11621..30514110 100644
--- a/src/arith/sidekick_arith.ml
+++ b/src/arith/sidekick_arith.ml
@@ -53,6 +53,9 @@ module type RATIONAL = sig
   val is_real : t -> bool
   (** A proper real, not nan/infinity *)
 
+  val is_int : t -> bool
+  (** Is this a proper integer? *)
+
   val pp_approx : int -> Format.formatter -> t -> unit
   (** Pretty print rational with given amount of precision
       (for example as a floating point number) *)
diff --git a/src/zarith/sidekick_zarith.ml b/src/zarith/sidekick_zarith.ml
index a3260b96..93f7b826 100644
--- a/src/zarith/sidekick_zarith.ml
+++ b/src/zarith/sidekick_zarith.ml
@@ -18,6 +18,7 @@ module Rational
   let infinity = Q.inf
   let minus_infinity = Q.minus_inf
   let is_real = Q.is_real
+  let is_int q = is_real q && Z.(equal (denum q) one)
 
   let pp_approx n out q = Format.fprintf out "%*.1f" n (Q.to_float q)
 end