GitLab

In the same style as most of the BI lemmas, e.g. `or_mono`, `and_mono`, ...

The types of propositions for monPred lemma need to be [monPred I PROP] and not [bi_car (monPredI I PROP)], otherwise iIntoValid fails in a very weird way. Seems to be related to a Coq bug.

BiIndexBottom class for bottom element in a bi index. monPred_all is a monoid morphism, and related big op lemmas.

Reorganize bi.monpred. Add unfolding manual lemmas for monPred_at, and use them in proofmode.monpred. Add big op lemmas for monpred_at.

Trying to improve IntoWand for monPred_car: whenever it's possible, we try to change the view automatically.