Apply 1 suggestion(s) to 1 file(s)

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.