diff --git a/Lebesgue/R_compl.v b/Lebesgue/R_compl.v
index 26f52f38c4fd165491f1d9aa0609dbb6bce21f13..f60e87eda59cdef64b340baac4864b82124608f6 100644
--- a/Lebesgue/R_compl.v
+++ b/Lebesgue/R_compl.v
@@ -760,7 +760,7 @@ Proof.
 apply Rmult_lt_0_compat; try apply pos_PI; lra.
 Qed.
 
-(** Providing statements from StdLib/Ratan with - (PI / 2), and not - PI / 2. *)
+(** Providing statements from Stdlib/Ratan with - (PI / 2), and not - PI / 2. *)
 
 Lemma minus_PI2 : - (PI / 2) = - PI / 2.
 Proof.