mathlib3

11cace15 - feat(data/real/ennreal): add instance linear_ordered_comm_monoid_with_zero ℝ≥0∞ (#15851)

feat(data/real/ennreal): add instance linear_ordered_comm_monoid_with_zero ℝ≥0∞ (#15851) Adding this instance also yields an instance of `zero_le_one_class` via type class inference, which gives access to `one_le_two`, so we remove `ennreal.one_le_two` in favor of `one_le_two`.