Commit 2024-01-01 07:00 0c9d4118

chore: Generalise monotonicity of multiplication lemmas to semirings (#9369) Many lemmas about BlahOrderedRing α did not mention negation. I could generalise almost all those lemmas to BlahOrderedSemiring α + ExistsAddOfLE α except for a series of five lemmas (left a TODO about them). Now those lemmas apply to things like the naturals. This is not very useful on its own, because those lemmas are trivially true on canonically ordered semirings (they are about multiplication by negative elements, of which there are none, or nonnegativity of squares, but we already know everything is nonnegative), except that I will soon add more complicated inequalities that are based on those, and it would be a shame having to write two versions of each: one for ordered rings, one for canonically ordered semirings. A similar refactor could be made for scalar multiplication, but this PR is big enough already. From LeanAPAP