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.

---

• depends on: feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas #17623

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

Adapted from #9250. This version is easier to review.

[github-actions]

PR summary b0223e31bb

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₀
+ Right.one_le_mul₀
+ Right.one_lt_mul_of_le_of_lt₀
+ Right.one_lt_mul_of_lt_of_le₀
+ Right.one_lt_mul₀
+ mul_le_one_left₀
+ mul_le_one_right₀
+ mul_lt_one_of_le_of_lt_of_pos_left
+ mul_lt_one_of_le_of_lt_right₀
+ mul_lt_one_of_le_of_lt₀
+ mul_lt_one_of_lt_of_le_left₀
+ mul_lt_one_of_lt_of_le_of_pos_right
+ mul_lt_one_of_lt_of_le₀
+ one_lt_mul₀

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.

[FR-vdash-bot]

I split the part that adds lemmas as #17623.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas #17623
  By Dependent Issues (🤖). Happy coding!