prime_in_gap

lemma prime_in_gap (a b : ℝ) (ha : 0 < a)    (h : ⌊a⌋₊.primeCounting < ⌊b⌋₊.primeCounting)    : ∃(p : ℕ), p.Prime ∧ a < p ∧ p ≤ b := by   have hab : ⌊a⌋₊ < ⌊b⌋₊ := Monotone.reflect_lt Nat.monotone_primeCounting h  obtain ⟨w, h, ha, hb⟩ := prime_in_gap' ⌊a⌋₊ ⌊b⌋₊ h  refine ⟨w, h, lt_of_floor_lt ha, ?_⟩  have : a < b := by    by_contra h    cases lt_or_eq_of_le <| le_of_not_gt h with    | inl hh => linarith [floor_le_floor <| le_of_lt hh]    | inr hh =>      rw [hh] at hab      rwa [←lt_self_iff_false ⌊a⌋₊]  by_contra h  have : ⌊b⌋₊ < w := floor_lt (by linarith) |>.mpr (lt_of_not_ge h)  have : ⌊b⌋₊ + 1 ≤ w := by linarith  linarith