inf_le_inf_left

Stream: general

[Yury G. Kudryashov]

I found out that inf_le_inf_left and sup_le_sup_left have different ideas about left/right. Which one do you prefer:
(a) left is a op b ≤ a op c;
(b) left is a op c ≤ b op c?

[Yury G. Kudryashov]

both add_le_add_left and mul_le_mul_of_nonneg_left use (a)

[Yury G. Kudryashov]

Same with sub_le_sub_left, mul_lt_mul_of_pos_left.

[Mario Carneiro]

I would suggest taking a tally of existing mathlib theorems to find consensus, which suggests (a)

[Bryan Gin-ge Chen]

#2109 is similar I guess.

[Kenny Lau]

inconsistencies like this are why I just try both variants (left and right) whenever I need to use such a theorem