naming for `left` and `right`

Stream: mathlib4

[Nailin Guan]

Is there a reason why add_le_add_left and add_le_add_right swap? Since I think left and rght should be the side differing from add_le_add?

[Damiano Testa]

Is this before or after #30242?

[Nailin Guan]

Exactly in 30242

[Damiano Testa]

I think that this is uniformising towards the convention at the end of Injectivity: left and right refer to what changes.

[Damiano Testa]

I am happy that there is some convention, but regardless of what the convention is, my algorithm is usually to try left first and, if I get a type mismatch, then I try right instead.

[Nailin Guan]

The only problem is when updating, never mind.