feat(algebra/ordered_ring): proof that `a + b ≤ a * b` (#6043)
This is Johan's proof of the fact above. If you are curious about the assumptions, there is an extensive discussion on
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology
