Ranges of Natural Numbers

[TOTBWF]

Description

This PR lays the groundwork for big operators by defining an API for working with ranges [x, y) of natural numbers, and proves some useful facts about them. It also does a bit of clean-up on Data.Nat.Properties.

[Lavenza]

Pull request preview

New pages

• Data.Nat.Range (+296, -0)
• Data.List.NonEmpty (+153, -0)

Changed pages

• Data.Nat.Properties (+190, -66)
• Data.List.Membership (+65, -1)
• Data.List.Properties (+48, -1)
• Data.Nat.DivMod (+20, -26)
• Data.List.Base (+14, -2)
• Data.Nat.Order (+8, -5)
• Data.Nat.Divisible.GCD (± 6)
• Data.Fin.Base (+11, -0)

[JacquesCarette]

A couple of typos.

[plt-amy]

Is this enough to prove that (Nat, ≤) is locally finite?

[TOTBWF]

You'll probably need something like map (k +_) (range i j) = range (k + i) (k + j) to displace the range down a standard finite set but that's pretty easy