proving equality related to floor division

Stream: new members

[Sabbir Rahman]

is there any easy strategy to prove floor division equalities where the fact that it's floor division is important. Take following example, the best idea I could come up is to reduce to a/n = b/n and prove both are 0. but that did make the proof unnecessarily long. A shorter proof is appreciated.

import Mathlib

example (x y : ℕ) (h: 3 < y) : (x * y + y + 1)/y = 1 + (x * y + 2)/y := by
  have : y > 0 := by positivity
  calc
    (x * y + y + 1) / y = (1 + (x + 1) * y) / y := by ring_nf
    _ = 1 / y + (x + 1) := by
      exact Nat.add_mul_div_right 1 (x + 1) this
    _ = 0 + (x + 1) := by
      congr
      refine Nat.div_eq_of_lt ?_; omega
    _ = 2 / y + (x + 1) := by
      congr 1
      refine (Nat.div_eq_of_lt ?_).symm; omega
    _ = 1 + (2 / y + x) := by ring
    _ = 1 + (2 + x * y) / y := by congr; exact Eq.symm (Nat.add_mul_div_right 2 x this)
    _ =  1 + (x * y + 2)/y := by ring_nf

[James Sundstrom]

Not sure about good general strategies, but here's my attempt at shortening the proof:

import Mathlib

example (x y : ℕ) (h: 3 < y) : (x * y + y + 1)/y = 1 + (x * y + 2)/y := by
  rw [mul_comm x, ← Nat.mul_add_one]
  repeat rw [Nat.mul_add_div, Nat.div_eq_zero_iff.mpr ∘ Or.inr]
  all_goals linarith