clean up / documentation

Stream: condensed mathematics

[Johan Commelin]

There are 84 lean files not in for_mathlib. I've decided that I should start cleaning them up and documenting them.
I've started with Mbar/bounded.lean. It's gone quite well.

You will be delighted to know that in the process, two new files were added to for_mathlib :crazy:

[Johan Commelin]

I'm quite happy with Mbar/* now. It now has a README.md that you can read over at https://github.com/leanprover-community/lean-liquid/tree/master/src/Mbar

[Johan Commelin]

I've removed over 100 lines of unused code, and replaced by linarith and by tidy with 1-line proofs where possible.

[Johan Commelin]

@Riccardo Brasca added has_nnnorm to mathlib. I've just gone through all of LTE. We now use nice notation $\|x\|_+$ for the norm as non-negative real number. It's used in ~ 100 places.