FKS2.FloorButhe.cover

theorem cover (s : ℝ) (h : s ∈ Set.Icc (2.236 : ℝ) 3.163) :    ∃ I ∈ slabs, s ∈ Set.Icc (I.lo : ℝ) I.hi := by  obtain ⟨hlo, hhi⟩ := h  set k : ℕ := ⌊(s - 2.236) / 0.05⌋₊ with hk_def  have hsub_nn : (0:ℝ) ≤ (s - 2.236) / 0.05 := by    apply div_nonneg <;> linarith  have hk_lt : k < 19 := by    have hub : (s - 2.236) / 0.05 < 19 := by      rw [div_lt_iff₀ (by norm_num)]; linarith    rw [hk_def]    exact Nat.floor_lt hsub_nn |>.mpr (by exact_mod_cast hub)  refine ⟨⟨2236/1000 + (k:ℚ)*50/1000, 2236/1000 + ((k:ℚ)+1)*50/1000, by    have hknn : (0:ℚ) ≤ (k:ℚ) := by exact_mod_cast Nat.zero_le k    linarith⟩, ?_, ?_⟩  · rw [slabs, List.mem_map]    exact ⟨k, List.mem_range.mpr hk_lt, rfl⟩  · have hfloor_le : (k : ℝ) ≤ (s - 2.236) / 0.05 := by      have := Nat.floor_le hsub_nn      rwa [← hk_def] at this    have hlt_floor : (s - 2.236) / 0.05 < (k : ℝ) + 1 := by      have := Nat.lt_floor_add_one ((s - 2.236) / 0.05)      rwa [← hk_def] at this    constructor    · push_cast      rw [le_div_iff₀ (by norm_num)] at hfloor_le      norm_num      linarith [hfloor_le]    · push_cast      rw [div_lt_iff₀ (by norm_num)] at hlt_floor      norm_num      linarith [hlt_floor]