Cover `mathlib` theorems for `RBMap`

[arienmalec]

mathlib RBTree and RBMap won't be ported to mathlib4 but some of the theorems there should eventually be covered in Std.

In particular:

https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/basic.lean

https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/find.lean

https://github.com/leanprover-community/mathlib/blob/master/src/data/rbtree/min_max.lean

https://github.com/leanprover-community/mathlib/blob/master/src/data/rbmap/default.lean