chore(Data/List/BigOperators): Use Std lemmas

[YaelDillies]

trafficstars

• Make Data.List.BigOperators.Basic, Data.List.Chain not depend on Data.Nat.Order.Basic by using Nat-specific Std lemmas rather than general mathlib ones. I leave the Data.Nat.Basic import since Data.List.BigOperators.Basic is algebra territory.
• As a consequence, move the order lemmas from Data.List.BigOperators.Basic to a newly created file Data.List.BigOperators.Order. Crediting Yakov for https://github.com/leanprover-community/mathlib/pull/8543.
• Also move the order lemmas from Data.List.BigOperators.Lemmas to Data.List.BigOperators.Order
• Also move the order lemmas from Algebra.BigOperators.Multiset.Lemmas to Algebra.BigOperators.Multiset.Order
• Make Data.List.BigOperators.Basic not depend on Algebra.Divisibility.Basic. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor.
• As a consequence, move the divisibility and MonoidWithZero lemmas from Data.List.BigOperators.Basic to Data.List.BigOperators.Lemmas.
• Move the content of Data.List.BigOperators.Defs to Mathlib.Data.List.BigOperators.Basic since no file imported the former without the latter and their imports are becoming very close after this PR.
• Make Data.List.Count, Data.List.Dedup, Data.List.ProdSigma, Data.List.Zip not depend on Data.List.BigOperators.Basic.
• As a consequence, move the big operators lemmas that were in there to Data.List.BigOperators.Basic. For the lemmas that were Nat -specific, keep a version of them stated using Nat.sum.
• To help with this, add Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum.

Before

After

---

• [ ] depends on: #11741