Segment lower bound

theorem segment_lower_bound (hm : StrictMono f) (h0 : f 0 = 0) (k : ℕ) :    f (segment f k) ≤ k := by  classical  rw [nth_of_strictMono hm (segment f k), segment]  rcases Classical.em (k ∈ range f) with h_k | h_k  · simp_all [count_succ_eq_succ_count]  · have h1 : count (· ∈ range f) k > 0 := count_notMem_range_pos h0 k h_k    have h2 : count (· ∈ range f) (k + 1) = count (· ∈ range f) k :=      count_succ_eq_count h_k    rw [h2]    suffices _ : nth (· ∈ range f) (count (· ∈ range f) k - 1) < k by omega    apply nth_lt_of_lt_count    omega