diff --git a/src/preludes/ria.ae b/src/preludes/ria.ae
index 2378572ae..0dafe50e5 100644
--- a/src/preludes/ria.ae
+++ b/src/preludes/ria.ae
@@ -56,6 +56,34 @@ theory Real_of_Int extends RIA =
      {i <= real_of_int(x)}.
      k <= x
 
+  (* floor(x) ≤ i iff x < i + 1 *)
+  axiom int_floor_ub:
+    forall x, y : real, i : int
+    [ int_floor(x), not_theory_constant(x), int_floor(x) in ]?, i], y |-> real_of_int(i + 1) ]
+    { int_floor(x) <= i }.
+    x < y
+
+  (* i <= floor(x) iff i <= x *)
+  axiom int_floor_lb:
+    forall x, y : real, i : int
+    [ int_floor(x), not_theory_constant(x), int_floor(x) in [i, ?[, y |-> real_of_int(i) ]
+    { i <= int_floor(x) }.
+    y <= x
+
+  (* ceil(x) ≤ i iff x ≤ i *)
+  axiom int_ceil_ub:
+    forall x, y : real, i : int
+    [ int_ceil(x), not_theory_constant(x), int_ceil(x) in ]?, i], y |-> real_of_int(i) ]
+    { int_ceil(x) <= i }.
+    x <= y
+
+  (* i <= ceil(x) iff i - 1 < x *)
+  axiom int_ceil_lb:
+    forall x, y : real, i : int
+    [ int_ceil(x), not_theory_constant(x), int_ceil(x) in [i, ?[, y |-> real_of_int(i - 1) ]
+    { i <= int_ceil(x) }.
+    y < x
+
    (* can add other axioms on strict ineqs on rationals ? *)
 
 end
diff --git a/tests/arith/ceil_floor_propagate.ae b/tests/arith/ceil_floor_propagate.ae
new file mode 100644
index 000000000..ef5959bdf
--- /dev/null
+++ b/tests/arith/ceil_floor_propagate.ae
@@ -0,0 +1,2 @@
+logic x: real
+goal g: int_ceil(x) = 0 and int_floor(x) = 0 -> x = 0.
diff --git a/tests/arith/ceil_floor_propagate.expected b/tests/arith/ceil_floor_propagate.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/arith/ceil_floor_propagate.expected
@@ -0,0 +1,2 @@
+
+unknown