Int.ofNat_ediv

theorem Int.ofNat_ediv : ∀ (m n : ℕ), ↑(m / n) = ↑m / ↑n

This theorem states that for any two natural numbers `m` and `n`, the integer representation of the division of `m` by `n` (`↑(m / n)`) equals to the division of the integer representation of `m` and `n` (`↑m / ↑n`). In other words, converting the result of the division of two natural numbers to an integer gives the same result as individually converting these two natural numbers to integers and then performing the division.

More concisely: For all natural numbers m and n, ⌊(m : ℕ) / n : ℕ⌋ = ⌊m:ℤ/⌈n:ℤ⌉⌋, where ℕ is the natural numbers, ℤ is the integers, and ⌋ and ⌈ denote the greatest integer function and the least integer function, respectively.