diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 7bd8fa78f7b8d134a4ed18b224c1fd59142c36d6..c2ea7fc4537ddb44ff13144edf03204cd09a8b93 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -354,6 +354,10 @@ Section lemmas.
               (atomic_acc Eo Ei α Pas β Φ).
   Proof. intros Helim. apply Helim. Qed.
 
+  (** Lemmas for directly proving one atomic accessor in terms of another (or an
+      atomic update).  These are only really useful when the atomic accessor you
+      are trying to prove exactly corresponds to an atomic update/accessor you
+      have as an assumption -- which is not very common. *)
   Lemma aacc_aacc {TA' TB' : tele} E1 E1' E2 E3
         α P β Φ
         (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index f670ca044a3c74e63fea9c09590315e25a3f4f71..3b5a49f7a73de52b12f73f8273bcdee4acc9716b 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -49,25 +49,34 @@ Section increment.
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
-  (** A proof of the incr specification that unfolds the definition
-      of atomic accessors.  Useful for introducing them as a concept,
-      but see below for a shorter proof. *)
+  (** A proof of the incr specification that unfolds the definition of atomic
+      accessors.  This is the style that most logically atomic proofs take. *)
   Lemma incr_spec_direct (l: loc) :
     ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
     (* Prove the atomic update for load *)
+    (* To [iMod] a *mask-changing* update (like "AU"), we have to unfold
+       [atomic_acc].
+       Note that [iInv] would work here without unfolding, i.e., an [AACC] in
+       the goal supports eliminating accessors but it does not support
+       eliminating mask-changing updates. *)
     rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
+    (* Usually, we would use [iAaccIntro], but here we cannot because we
+       unfolded [atomic_acc], so we do it by hand. *)
     iModIntro. iExists _, _. iFrame "Hl". iSplit.
     { (* abort case *) done. }
     iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro.
     (* Now go on *)
     wp_pures. awp_apply cas_spec; first done.
-    (* Prove the atomic update for CAS *)
+    (* Prove the atomic update for CAS. We want to prove the precondition of
+       that update (the ↦) as quickly as possible because every step we take
+       along the way has to be "reversible" to prove the "abort" update. *)
     rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
     iModIntro. iExists _. iFrame "Hl". iSplit.
     { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
+    (* Good, we proved the precondition, now we can proceed "as normal". *)
     iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
     - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
       iIntros "!>". wp_if. by iApply "HΦ".
@@ -75,8 +84,11 @@ Section increment.
       iIntros "!>". wp_if. iApply "IH". done.
   Qed.
 
-  (** A proof of the incr specification that uses lemmas to avoid reasining
-      with the definition of atomic accessors. *)
+  (** A proof of the incr specification that uses lemmas ([aacc_aupd_*]) to
+      avoid reasining 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. *)
   Lemma incr_spec (l: loc) :
     ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.