feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 (#4363)
Per [discussion](https://github.com/leanprover-community/mathlib/pull/4296#issuecomment-701953077) in #4296.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
