Add more Data.Rational.Properties

[kleinreact]

I needed the following common properties over normalized rationals for some proofs, but found them to be missing in the library.

↥[i/1]≡i        : (i : ℤ) → ↥ (i / 1) ≡ i
↧ₙ[i/1]≡1       : (i : ℤ) → ↧ₙ (i / 1) ≡ 1
n/n≡1           : ∀ (n : ℕ) .{{_ : ℕ.NonZero n}} → + n / n ≡ 1ℚ
-i/n≡-[i/n]     : ∀ (i : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n}} →
                  ℤ.- i / n ≡ - (i / n)
*-cancelˡ-/     : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (p ℕ.* r)}} →
                  (+ p ℤ.* q) / (p ℕ.* r) ≡ q / r
*-cancelʳ-/     : ∀ p {q r} .{{_ : ℕ.NonZero r}} .{{_ : ℕ.NonZero (r ℕ.* p)}} →
                  (q ℤ.* + p) / (r ℕ.* p) ≡ q / r
i/n+j/n≡[i+j]/n : ∀ (i j : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n }} →
                  i / n + j / n ≡ (i ℤ.+ j) / n

Hence, my proposal to add them with this PR.