diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index e704f284f2247f9513c08341fe7939de3df0b7b2..0fdee4cd0327ae37ce5dc13657f486146e8898ac 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -86,7 +86,7 @@ Section increment.
   Qed.
 
   (** A proof of the incr specification that uses lemmas ([aacc_aupd_*]) to
-      avoid reasining with the definition of atomic accessors. These lemmas are
+      avoid reasoning with the definition of atomic accessors. These lemmas are
       only usable here because the atomic update we have and the one we try to
       prove are in 1:1 correspondence; most logically atomic proofs will not be
       able to use them. *)