left/right naming

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#Set.diff_subset_diff_left and docs#sdiff_le_sdiff_right. They're defeq (for sets). Do we have a policy about left/right in lemmas like this?

[Yaël Dillies]

For some weird reason, we need the Set/Finset-specific lemmas for rewriting

[Yury G. Kudryashov]

Even if we drop Set/Finset-specific lemmas (e.g., by migrating to ≤ with notation), we have plenty of other opportunities to be inconsistent with left/right in the names.

[Yaël Dillies]

For left/right questions about binary operators, please always follow docs#mul_le_mul_of_nonneg_left and docs#mul_le_mul_of_nonneg_right. I spent a lot of time ensuring the left/right naming is consistent within the order theory of multiplication.