diff --git a/theories/Reals/Cauchy/PiCosZeroSeqProbe.v b/theories/Reals/Cauchy/PiCosZeroSeqProbe.v
index b6ec6ffa2f..975bf004bf 100644
--- a/theories/Reals/Cauchy/PiCosZeroSeqProbe.v
+++ b/theories/Reals/Cauchy/PiCosZeroSeqProbe.v
@@ -46,3 +46,5 @@ Definition cos_zero_seq (n : nat) : Q :=
   proj1_sig (approx_root_cos (log_eps n) (log_eps_pos n)).
 
 Print Assumptions cos_zero_seq.
+
+(* ci dress rehearsal: gpg-signed commit verification *)