diff --git a/util/nat.v b/util/nat.v
index 7fa4adfc23d635b930e3411b4e1643207606216d..7bedb25bd0d3548e33e4facc0bb817c0fa1d68fc 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -6,9 +6,9 @@ Require Export prosa.util.tactics.
 (** Additional lemmas about natural numbers. *)
 Section NatLemmas.
 
-  (** First, we show that, given [m1 >= m2] and [n1 >= n2], an
-      expression [(m1 + n1) - (m2 + n2)] can be transformed into
-      expression [(m1 - m2) + (n1 - n2)]. *)
+  (** First, we show that, given [m >= p] and [n >= q], an
+      expression [(m + n) - (p + q)] can be transformed into
+      expression [(m - p) + (n - q)]. *)
   Lemma subnACA m n p q : p <= m -> q <= n ->
     (m + n) - (p + q) = (m - p) + (n - q).
   Proof. by move=> plem qlen; rewrite subnDA addnBAC// addnBA// subnAC. Qed.