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".