use Proper and rewrite from stdlib for monotonicity

[haansn08]

This PR replaces the monotonic predicate with Proper (le ==> le) from stdlib.

Pros:

• one can use setoid_rewrite and setoid_replace for upper bounding expressions instead of using the custom poly_mono tactic + existential variables.
• monotonicity of nat -> nat functions can be shown by the solve_proper tactic from stdlib instead of using smpl which has been dropped from the depedencies of coq-library-undecidability (smpl is still needed for other things however).

Pros?:

• the monotonicity instances are now separate from inOPoly lemmas.
• smpl_inO is weaker and only proves inOPoly instead of of both monotonic and inOPoly which are often used together.

Cons:

• Proper (le ==> le) is more verbose and arguably harder to understand than monotonic.
• Rewrite / Typeclass resolution can get hard to understand hiccups which was not the case with the custom smpl tactic.