[Add] Division properties for Nat, Integer, and Rational

[aortega0703]

Hi, I saw there weren't many properties for division outside of Naturals so I went ahead and proved some for (Unnormalised) Rationals and Integers (and Naturals too):

Data.Rational.Unnormalised:

• /-distribʳ-+: fractions with sums on the numerator can be "split" into sums of fractions
• n/d≡[n/1]*[1/d]: this was more of a convenience to prove /-distribʳ-+ but I thought it could be useful enough to add it separately (maybe not?).
• /-monoˡ-<, /-monoʳ-<-pos, /-monoʳ-<-neg, /-monoˡ-≤, /-monoʳ-≤-nonNeg, and /-monoʳ-≤-nonPos: In Rational denominators are ℕs, so there isn't a sign hell as with Integer.

Data.Integer.DivMod:

• n<0⇒n/ℕd<0: there was already 0≤n⇒0≤n/ℕd so I added "the other case".
• 0/d≡0 and n/1≡n (also for /ℕ).
• n/ℕd≡0⇒∣n∣<d and n/d≡0⇒∣n∣<∣d∣: the integer version of m/n≡0⇒m<n.
• 0≤n<d⇒n/d≡0 (also /ℕ): the "converse" (not really), an int version of m<n⇒m/n≡0.
• /ℕ-monoˡ-≤ (and helpers), /ℕ-monoʳ-≤-nonNeg and /ℕ-monoʳ-≤-nonPos.
• /-monoˡ-≤-pos and /-monoˡ-≤-neg: I put a reduntant NonZero to make _/_ happy where only Positive/Negative should really suffice. I admit I tried deriving the NonZero but I don't know how to do it without making the type too verbose/ugly.
• /-monoʳ-≤-nonNeg-eq-signs and /-monoʳ-≤-nonPos-eq-signs: The proofs for these are basically the same, extremely so (just swapping the denominators names), but I can't figure a way to prove one with the other. (- n) / d and - (n / d) are not always equal so I can't just convert the numerator from nonPos to nonNeg, but maybe there's another way?
• /-monoʳ-≤-nonNeg-op-signs and /-monoʳ-≤-nonPos-op-signs: I also noticed how /-monoʳ-≤-nonNeg-eq-signs and /-monoʳ-≤-nonPos-op-signs have basically the same type (their counterparts too) but I don't know If it's better to keep them separate or combine them and ask for something like sign (n * d₁ * d₂) ≡ Sign.+ in the type.

Data.Nat.DivMod:

• sn%d≡0⇒sn/d≡s[n/d] and sn%d>0⇒sn/d≡n/d: These really really (really) helped to reason about Integer division. Also, they are nice in that they describe whether the quotient increases with the dividend or it stays the same.
• %-pred-≡suc: This is "the other case" of %-pred-≡0, it says that the remainder increases on par with the dividend (exept for the jump at remainder 0). I don't like the name on this one but I retained the name style of %-pred-≡0.

I have yet to translate the Unnormalised proofs to normalised Rationals and I'm not sure about the whole deal with the signs on the types for /-mono on Integers so it's a draft for now.

[JacquesCarette]

Nice. Some of the proofs seem to go rather "low level" though.

[jamesmckinna]

@aortega0703 are you planning to return to this?

[aortega0703]

@aortega0703 are you planning to return to this?

Hi, yes! sorry for disappearing there. I just made the last proofs that I wanted for this PR (translating what I did for Rational.Unnormalized to Rational). After updating the README I just realized that in the meantime a proof for /-distribʳ-+ was added in #2996 (under the name i/n+j/n≡[i+j]/n). I like mine better, but which one should I keep (and under what name)?