mathlib

6ccfe5a3 - feat(algebra/ordered...): Two tiny lemmas (#1522)

feat(algebra/ordered...): Two tiny lemmas (#1522) * feat(algebra/ordered...): Two tiny lemmas * style(src/algebra/ordered_field) Co-Authored-By: Reid Barton <rwbarton@gmail.com>