diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 35430b246696f616d371d1ee70960a1c5cc23801..66839c4d6239d1264aadcbcb5f7203af56c776cd 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -365,4 +365,17 @@ Section monotonicity.
       rewrite Hst in Hsl, Hed |- *.
       now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')).
   Qed.
+
+  Theorem is_monotonic :
+    forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) ->
+                 state_leb (st, n) (st', n') = true ->
+                 compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+  Proof.
+    intros n n' He He' Hsl.
+    pose proof (instr_kind_is_comparable e e') as Heqd.
+
+    destruct Heqd as [Heq | Hdiff].
+    - now apply (unmoved_can_advance n).
+    - now apply (moved_lat_is_lower n n').
+  Qed.
 End monotonicity.