Erdos392.Params.initial.smooth_of_dvd_small_prime

lemma Params.initial.smooth_of_dvd_small_prime (P : Params) {p m : ℕ} (hp : p ≤ Real.sqrt P.n)    (hpL : p > P.L) (hm : m ∈ Finset.Ico (P.n - P.n / P.M) P.n) (hpm : p ∣ m) :    m ∈ (P.n / P.L).smoothNumbers := by  by_contra h_not_smooth  have hm_ne_zero : m ≠ 0 := by    intro h    rw [Finset.mem_Ico, h, nonpos_iff_eq_zero, Nat.sub_eq_zero_iff_le] at hm    nlinarith [div_mul_le_self P.n P.M, P.hM, P.hL_pos, P.hL, P.hL']  obtain ⟨q, hq_prime, hq_div, hq_ge⟩ : ∃ q, q.Prime ∧ q ∣ m ∧ q ≥ P.n / P.L := by    simp only [smoothNumbers] at h_not_smooth    simp_all  have hp_div_mq : p ∣ m / q := by    refine dvd_div_of_mul_dvd <| Coprime.mul_dvd_of_dvd_of_dvd      (hq_prime.coprime_iff_not_dvd.mpr fun h ↦ ?_) hq_div hpm    rw [le_sqrt (cast_nonneg _) (cast_nonneg _)] at hp    norm_cast at hp    nlinarith [le_of_dvd (lt_trans P.hL_pos hpL) h, div_add_mod P.n P.L, mod_lt P.n P.hL_pos]  have hm_gt_n : P.n < m := by    rw [(Nat.mul_div_cancel' hq_div).symm]    refine lt_of_lt_of_le ?_ (Nat.mul_le_mul hq_ge <| lt_of_lt_of_le hpL <| le_of_dvd (div_pos      (le_of_dvd (pos_of_ne_zero hm_ne_zero) hq_div) hq_prime.pos) hp_div_mq)    nlinarith only [div_add_mod P.n P.L, mod_lt P.n (pos_of_ne_zero      (by linarith [P.hL_pos] : P.L ≠ 0)), P.hL_pos, P.hL]  linarith [Finset.mem_Ico.mp hm]