γ₃_lower_bound

lemma γ₃_lower_bound (n : ℕ) (hn : 1 ≤ n) :    γ₃ n < Real.eulerMascheroniConstant := by  have h_strict_mono : StrictMono (fun n : ℕ => γ₃ (n + 1)) :=    strictMono_nat_of_lt_succ (fun k => γ₃_increasing (k + 1) (by omega))  have h_tendsto : Filter.Tendsto (fun n : ℕ => γ₃ (n + 1))      Filter.atTop (nhds eulerMascheroniConstant) :=    γ₃_tendsto.comp (Filter.tendsto_add_atTop_nat 1)  have h_lt : ∀ k : ℕ, γ₃ (k + 1) < eulerMascheroniConstant := fun k =>    lt_of_lt_of_le      (h_strict_mono <| Nat.lt_succ_self _)      (ge_of_tendsto h_tendsto <| Filter.eventually_atTop.mpr        ⟨k + 1, fun m hm => h_strict_mono.monotone hm⟩)  cases n with  | zero => omega  | succ m => exact h_lt m