chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use ZeroLEOneClass

[FR-vdash-bot]

There are still some useless lemmas that were simply ported from Algebra.Order.Monoid.Lemmas, such as just chain an existing lemma with an assumption and lemmas whose assumptions imply 1 ≤ 0. This PR removes them.

Also, some lemmas have both assumptions like 1 < a 0 < a. This PR uses ZeroLEOneClass to remove redundant assumptions.

---

Ported from leanprover-community/mathlib3#16525 and leanprover-community/mathlib3#18158

[urkud]

Could you please deprecate them instead?

[github-actions]

PR summary 09a72c1f57

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Left.one_le_mul₀
+ Left.one_lt_mul_of_le_of_lt₀
+ Left.one_lt_mul_of_lt_of_le₀
+ Left.one_lt_mul₀
+ Left.zero_lt_one_of_pos
+ Right.one_le_mul₀
+ Right.one_lt_mul_of_le_of_lt₀
+ Right.one_lt_mul_of_lt_of_le₀
+ Right.one_lt_mul₀
+ Right.zero_lt_one_of_pos
+ mul_le_one
+ mul_le_one_left
+ mul_le_one_right
+ mul_lt_one_left
+ mul_lt_one_of_le_of_lt_left
+ mul_lt_one_of_le_of_lt_right
+ mul_lt_one_of_lt_of_le_left
+ mul_lt_one_of_lt_of_le_right
+ mul_lt_one_right
+ one_le_mul_of_le_of_le
+ one_lt_mul_of_lt_of_lt
+ zero_lt_one_of_pos

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.