mathlib3

4e19dab9 - chore(algebra/order/ring): Normalize `_left`/`_right` (#14985)

chore(algebra/order/ring): Normalize `_left`/`_right` (#14985) Swap the `left` and `right` variants of * `nonneg_of_mul_nonneg_` * `pos_of_mul_pos_` * `neg_of_mul_pos_` * `neg_of_mul_neg_`