diff --git a/theories/numbers.v b/theories/numbers.v
index 8b282be15fb43a24a6b3d246726135d8b12e3b35..4f72314302e0bfea69cae39fd9fda484d4e258cc 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -65,10 +65,10 @@ Proof. unfold lt. apply _. Qed.
 Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
 Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
 
-(* [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
+(** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
 Lemma nat_minus_plus n m : n + m - n = m.
 Proof. lia. Qed.
-(* [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
+(** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
 Lemma nat_le_plus_minus n m : n ≤ m → m = n + (m - n).
 Proof. lia. Qed.