Make `iNext` smarter for mixed `▷` and `▷^(n+m)`

Following the (fixed) issue (https://gitlab.mpi-sws.org/FP/iris-coq/issues/141), there is still an error w.r.t. addition in the laterN modality:

From iris Require Import proofmode.tactics.

Lemma foo {M} (P : uPred M) n m : ▷ ▷^(n+m) P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.

(* Gives

"H" : ▷ ▷^(n + m) P
--------------------------------------∗
▷ P
*)

forgetting erroneously to cancel n in the premise "H".