rw [h, ←Int.add_assoc, Int.add_right_comm]
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ j
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ i + 1 + ofNat n