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

Reviewed-by: gares

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 853ddfd6dc..46215f16a6 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2222,14 +2222,14 @@ 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_{n + 1 − k}` and the
+      in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the
       circular order of subgoals remains unchanged.
 
    .. tacn:: first @num last
 
       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. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order
       of subgoals remains unchanged.
 
 Finally, the tactics ``last`` and ``first`` combine with the branching syntax