[Typo] Section 8.5 recursion on wrong var in Nat.plusR rhs

def Nat.plusR : Nat → Nat → Nat
  | n, 0 => n
  | n, k + 1 => plusR n k + 1

The recursion doesn't reduce the size of either Nat and generates a "Failed to show termination" error. I believe the last line should be

  | n, k + 1 => plusRinbook (n + 1) k 

Full error text:

▶ 8:5-8:14: error:
fail to show termination for
  Nat.plusR
with errors
failed to infer structural recursion:
Cannot use parameter #1:
  failed to eliminate recursive application
    n.plusR (k + 1)
Cannot use parameter #2:
  failed to eliminate recursive application
    n.plusR (k + 1)

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            x1 x2
1) 10:16-31  =  =
Please use `termination_by` to specify a decreasing measure.

Open Section 8.5 and inspect the Nat.plusR example shown in the issue. Correct the recursive right-hand side as indicated, then verify that the example no longer reports the displayed termination error.