chore(Algebra/Order/Ring/Lemmas): resolving name inconsistencies

[FR-vdash-bot]

This PR allows the names to be clearly distinguished from versions that do not require positivity assumptions, but also become too long.

Due to name conflicts, some similar lemmas have dissimilar names before this PR:

theorem mul_lt_mul_of_nonneg_of_pos [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d
theorem mul_lt_mul_of_le_of_lt' [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (b0 : 0 ≤ b) (c0 : 0 < c) : a * c < b * d

Statement	New name	Old name
a * c ≤ b * d	mul_le_mul_of_le_of_le_of_nonneg_of_nonneg	mul_le_mul_of_le_of_le
	mul_le_mul_of_le_of_le_of_nonneg_of_nonneg'	mul_le_mul (still there)
a * c < b * d	mul_lt_mul_of_le_of_lt_of_pos_of_nonneg	mul_lt_mul_of_pos_of_nonneg
	mul_lt_mul_of_le_of_lt_of_nonneg_of_pos	mul_lt_mul_of_le_of_le' / mul_lt_mul' (still there)
	mul_lt_mul_of_lt_of_le_of_nonneg_of_pos	mul_lt_mul_of_nonneg_of_pos
	mul_lt_mul_of_lt_of_le_of_pos_of_nonneg	mul_lt_mul_of_le_of_lt' / mul_lt_mul (still there)
	mul_lt_mul_of_lt_of_lt_of_pos_of_pos	mul_lt_mul_of_pos_of_pos
	mul_lt_mul_of_lt_of_lt_of_pos_of_pos'	mul_lt_mul_of_lt_of_lt'
	(Left.)mul_lt_mul_of_lt_of_lt_of_nonneg_of_nonneg	mul_lt_mul'' (still there)
	Right.mul_lt_mul_of_lt_of_lt_of_nonneg_of_nonneg
a * b < 0 → 0 ≤ b → a < 0	(Left.)neg_of_mul_neg_left	neg_of_mul_neg_left / Left.neg_of_mul_neg_right
	Right.neg_of_mul_neg_left	Right.neg_of_mul_neg_right
a * b < 0 → 0 ≤ a → b < 0	(Left.)neg_of_mul_neg_right	neg_of_mul_neg_right / Left.neg_of_mul_neg_left
	Right.neg_of_mul_neg_right	Right.neg_of_mul_neg_left

Lines 304 - 321 and 476 - 495 were just moved together.

Some variable names are changed to be consistent with the rest of the file.

If there is a better way to resolve name conflicts, please feel free to comment.

---

Split from #9249

Zulip