integer in an interval

Stream: Is there code for X?

[Alex Kontorovich]

Is there a slick way to prove this? If two real numbers differ by at least 1, then either there's an integer strictly between them, or they're consecutive integers:

import Mathlib

example (a b : ℝ) (hab : 1 ≤ b - a) :
    (∃ (k : ℤ), a < k ∧ k < b) ∨ (∃ (k : ℤ), a = k ∧ b = k + 1) := by
  sorry

[Michael Stoll]

Take k as the ceiling of a and case on whether a = k or not?

[Michael Stoll]

OK; there is a secondary case when a = k ... But it should not be too cumbersome.

[Yaël Dillies]

import Mathlib

example (a b : ℝ) (hab : 1 ≤ b - a) :
    (∃ (k : ℤ), a < k ∧ k < b) ∨ (∃ (k : ℤ), a = k ∧ b = k + 1) := by
  rw [le_sub_iff_add_le'] at hab
  obtain ha | ha := (Int.le_ceil a).gt_or_eq
  · have := Int.ceil_lt_add_one a
    exact .inl ⟨⌈a⌉, ha, by linarith⟩
  obtain rfl | hab := hab.eq_or_lt
  · exact .inl ⟨⌈a⌉, by simp [ha]⟩
  · refine .inl ⟨⌈a⌉ + 1, ?_, ?_⟩ <;> push_cast <;> linarith

[Michael Stoll]

import Mathlib

example (a b : ℝ) (hab : 1 ≤ b - a) :
    (∃ (k : ℤ), a < k ∧ k < b) ∨ (∃ (k : ℤ), a = k ∧ b = k + 1) := by
  let k := ⌈a⌉
  by_cases h : a = k
  · by_cases h' : b = k + 1
    · exact .inr ⟨k, h, h'⟩
    · refine .inl ⟨k+1, by rw[h]; exact_mod_cast Int.lt_succ k, ?_⟩
      push_cast
      linarith (config := {splitNe := true})
  · have ha : a ≤ k := Int.le_ceil a
    have hk : k < a + 1 := Int.ceil_lt_add_one a
    refine .inl ⟨k, ?_, ?_⟩ <;>
      linarith (config := {splitNe := true})

This can certainly be golfed somewhat...

[Yaël Dillies]

I think we have basically the same solution

[Michael Stoll]

Yeah, I guess the informal proof is quite clear...