Commit 2021-10-13 15:48 577cac15

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.