mathlib

1cf59fcc - chore(src/algebra/ordered_ring.lean): fix linting errors (#2827)

chore(src/algebra/ordered_ring.lean): fix linting errors (#2827) [Mentioned, but not really discussed, in this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20get.20familiar.20enough.20with.20Mathlib.20to.20use.20it/near/198747067). This PR also removes `mul_pos'` and `mul_nonneg'` lemmas because they are now identical to the improved `mul_pos` and `mul_nonneg`.