mathlib

6f1d90d3 - feat(algebra/order/monoid_lemmas_gt_zero): introduce the type of positive elements and prove some lemmas (#11833)

feat(algebra/order/monoid_lemmas_gt_zero): introduce the type of positive elements and prove some lemmas (#11833) This PR continues the `order` refactor. Here I start working with the type of positive elements of a type with zero and lt. Combining `covariant_` and `contravariant_classes` where the "acting" type is the type of positive elements, we can formulate the condition that "multiplication by positive elements is monotone" and variants. I also prove some initial lemmas, just to give a flavour of the API. More such lemmas will come in subsequent PRs (see for instance #11782 for a few more lemmas). After that, I will start simplifying existing lemmas, by weakening their assumptions.