Rename laterN_plus into laterN_add
The following discussion from !808 (merged) should be addressed:
-
@robbertkrebbers started a discussion: (+1 comment) Hmm, we already have:
Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
So, with plus instead of add.
Since the new convention in Coq is to use add, maybe the laterN lemma should be renamed?