Make invariants closed under weakening.
As requested in #112 (closed) this gives:
Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q.
But even more:
Lemma inv_split N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
This solves one half of #112 (closed).