mathlib

ad680c24 - chore(algebra/ordered_ring): remove duplicate lemma (#4295)

chore(algebra/ordered_ring): remove duplicate lemma (#4295) `ordered_ring.two_pos` and `ordered_ring.zero_lt_two` had ended up identical. I kept `zero_lt_two`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>