mathlib

577cac15 - feat(algebra/order/nonneg): properties about the nonnegative cone (#9598)

feat(algebra/order/nonneg): properties about the nonnegative cone (#9598) * Provide various classes on the type `{x : α // 0 ≤ x}` where `α` has some order (and algebraic) structure. * Use this to automatically derive the classes on `nnreal`. * We currently do not yet define `conditionally_complete_linear_order_bot nnreal` using nonneg, since that causes some errors (I think Lean then thinks that there are two orders that are not definitionally equal (unfolding only instances)). * We leave a bunch of `example` lines in `nnreal` to show that `nnreal` has all the old classes. These could also be removed, if desired. * We currently only give some instances and simp/norm_cast lemmas. This could be expanded in the future. Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu> Co-authored-by: Johan Commelin <johan@commelin.net>