Add monadic `;;` and change level of the do-notation to 100

While trying to port some of the IPM tactics from Ltac to Mtac2 (formerly MetaCoq) I ran into the issue that _ ;; _ was used at a different level in both Iris and Mtac2, making it impossible to combine both projects. The current levels are as follows:

	_ ;; _	_ <- _; _
std++	not present	65
Iris's heap_lang	100	not present
Mtac2	81	81

As you can see, the levels are all different!

Some notes:

• I think _ ;; _ and _ <- _; _ should be at the same level.

• The notation _ ;; _ is not present in stdpp, but it should be there:

Notation "x ;; z" := (x ≫= λ _, z).

• If we currently add this notation, using the same level as _ <- _; _, namely 65, it will currently Iris.

This MR changes the level of _ <- _; _ in std++ into 100, which is consistent with Iris. When we accept this MR, a one line fix for Iris is needed.

The main consequence of this MR is how these notations will interact with equality. Consider:

m1 = m2 ;; m3

Should that be parsed as:

1. (m1 = m2) ;; m3 (now)
2. m1 = (m2 ;; m3) (before)

I'd say that when the notation is used for an imperative programming language, like Iris's heap_lang, it should definitely be (1). However, in the case of monadic code, (1) makes very little sense (at least for equality, but maybe it makes sense for other relations), as it will never type check.

Note that many other relations like setoid equality and inequality of numbers are also at level 70.