Factor out lemma `löb_weak`.

This MR adds the lemma:

Lemma löb_weak : BiLöb PROP ↔ ∀ P, (▷ P ⊢ P) → (True ⊢ P).

This lemma was implicit as part of the proof later_contractive_bi_löb. Since it's an interesting result on its own, I factored it out as a separate lemma. I also stated the result as a bi-implication (the left-to-right implication is trivial, though).

I also improved the comments.