The plausibly modality

Much of this is based on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/184#note_31510 by @amintimany, but made to work for non-affine BIs and changed in such a way that it follows the Iris naming conventions.

Some TODOs:

• Should the modality be affine or absorbing?
• Could we change the definition so that the following result holds even if P is not absorbing:

  Lemma plain_plausibly P `{!Plain P, !Absorbing P} : <plausible> P ⊣⊢ P.

• The properties that the modality commutes with ▷ and ∀ are pretty useless because they only hold when the proposition inside is plain (they thus trivially follow from plain_plausibly). Do we have such lemmas in general for some connectives? Otherwise, I propose to remove these lemmas.
• It would be useful to have some proof mode instances to support easy reasoning using the modality. @amintimany has some in his post, but what we had is not complete.

cc @jtassaro