diff --git a/theories/numbers.v b/theories/numbers.v
index 0824477f665e2279abcd3439b1d2620934244dc3..13e32b54a114e4d81359de124edb8f86deadb1dc 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -724,7 +724,7 @@ Local Close Scope Qc_scope.
 (** We define the type [Qp] of positive rationals as fractions of positives with
 an [SProp]-based proof that ensures the fraction is in canonical form (i.e., its
 gcd is 1). Note that we do not define [Qp] as a subset (i.e., Sigma) of the
-standard library's [Qc]. The type [Qc] uses a [Prop]-based proof for canonicity
+standard library's [Qc] because the type [Qc] uses a [Prop]-based proof (not [SProp]) for canonicity
 of the fraction. *)
 Definition Qp_red (q : positive * positive) : positive * positive :=
   (Pos.ggcd (q.1) (q.2)).2.