mathlib3

feat (analysis/normed_space/basic.lean): implement reverse triangle inequality

#831

Merged