Fix off-by-one in docs of `first num last` (fix #11463)

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 853ddfd6dc..6d3259bb4d 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2229,7 +2229,7 @@ tactics to *permute* the subgoals generated by a tactic.
 
       If :token:`num`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
-      in focus. The first subgoal becomes :math:`G_k` and the circular order
+      in focus. The first subgoal becomes :math:`G_{k + 1 \bmod n}` and the circular order
       of subgoals remains unchanged.
 
 Finally, the tactics ``last`` and ``first`` combine with the branching syntax