feat(algebra/ordered_ring): ask for 0 < 1 earlier. (#4296)
It used to be that `linear_ordered_semiring` asked for `0 < 1`, while `ordered_semiring` didn't.
I'd prefer that `ordered_semiring` asks for this already:
1. because lots of interesting examples (e.g. rings of operators) satisfy this property
2. because the rest of mathlib doesn't care
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
