chore(Data/List): Depend less on big operators

[YaelDillies]

trafficstars

• Make Data.List.Count, Data.List.Dedup, Data.List.ProdSigma, Data.List.Range, Data.List.Rotate, 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 themin the original file but stated using Nat.sum.
• To help with this, add Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum.

---