Erdos392.Params.initial.div_le

lemma Params.initial.div_le (P : Params) (m : ℕ) (hm : m ∈ P.initial.a) :    (P.n : ℝ) / m ≤ (1 - 1 / (P.M : ℝ))⁻¹ := by  have ⟨hlo, hhi⟩ := mem_range P m hm  have hM_pos : (0 : ℝ) < P.M := Nat.cast_pos.mpr (Nat.zero_lt_of_lt P.hM)  have h_denom_pos : 0 < 1 - 1 / (P.M : ℝ) := by    rw [sub_pos, div_lt_one hM_pos]; exact Nat.one_lt_cast.mpr P.hM  have hn_pos : (0 : ℝ) < P.n :=    Nat.cast_pos.mpr (Nat.lt_of_lt_of_le (P.initial.hpos m hm) hhi.le)  have hlo' : (P.n : ℝ) - P.n / P.M ≤ m := by    calc (P.n : ℝ) - P.n / P.M ≤ P.n - (P.n / P.M : ℕ) := by gcongr; exact Nat.cast_div_le      _ = ((P.n - P.n / P.M : ℕ) : ℝ) := by rw [Nat.cast_sub (Nat.div_le_self ..)]      _ ≤ m := by exact_mod_cast hlo  calc (P.n : ℝ) / m ≤ P.n / (P.n - P.n / P.M) := by        gcongr; rw [sub_pos]; exact div_lt_self hn_pos <| one_lt_cast.mpr P.hM    _ = P.n / (P.n * (1 - 1 / (P.M : ℝ))) := by rw [mul_sub, mul_one, mul_one_div]    _ = (1 - 1 / (P.M : ℝ))⁻¹ := by rw [div_mul_eq_div_div, div_self hn_pos.ne', one_div]