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