FKS2.coverFrom

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