mathlib

62740866 - refactor(algebra/order/{monoid_lemmas_zero_lt + ring} + crumbs) remove duplicate lemmas (#16189)

refactor(algebra/order/{monoid_lemmas_zero_lt + ring} + crumbs) remove duplicate lemmas (#16189) This is one of the cleaning up stages of the `order` refactor. This PR removes some of the lemmas for ordered semirings that are now superfluous. To keep things simple, the new lemmas are in the `zero_lt` namespace and we export this namespace. Probably, this will not stay this way once the tide of unsuccessful builds washes away. The plan for this PR is to align names and order of explicit hypotheses in the `zero_lt` file with the lemmas in `ring`, in order to delete them. This will likely involve changing a few extra files, but I'm hoping to seriously contain the diff outside of these two files. I want to thank @negiizhao who has been a great help in taking over and pushing forward the refactor!