Commit 2022-02-23 10:50 6f1d90d3

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.