…d_eq_of_le_of_le_of_mul_le` earlier (#6483)

This move was suggested in #6220.  In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.

Affected files:
```
Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic
```

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221).

The signature of a theorem changed:
```lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`
```
Modified files:
```
Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf
```

…d_eq_of_le_of_le_of_mul_le` earlier (#6483)

This move was suggested in #6220.  In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.

Affected files:
```
Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic
```

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221).

The signature of a theorem changed:
```lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`
```
Modified files:
```
Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf
```

…d_eq_of_le_of_le_of_mul_le` earlier (#6483)

This move was suggested in #6220.  In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.

Affected files:
```
Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic
```

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221).

The signature of a theorem changed:
```lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`
```
Modified files:
```
Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf
```