Commit 2024-04-07 07:06 47062a71

chore: Split Data.{Nat,Int}{.Order}.Basic in group vs ring instances (#11924) Scatter the content of Data.Nat.Basic across:

• Data.Nat.Defs for the lemmas having no dependencies
• Algebra.Group.Nat for the monoid instances and the few miscellaneous lemmas needing them.
• Algebra.Ring.Nat for the semiring instance and the few miscellaneous lemmas following it. Similarly, scatter
• Data.Int.Basic across Data.Int.Defs, Algebra.Group.Int, Algebra.Ring.Int
• Data.Nat.Order.Basic across Data.Nat.Defs, Algebra.Order.Group.Nat, Algebra.Order.Ring.Nat
• Data.Int.Order.Basic across Data.Int.Defs, Algebra.Order.Group.Int, Algebra.Order.Ring.Int Also move a few lemmas from Data.Nat.Order.Lemmas to Data.Nat.Defs. Before After