Erdos392.Params.initial.count_multiples_lower_bound

lemma Params.initial.count_multiples_lower_bound (n M p : ℕ) (hM : M > 0) (hp : p > 0) :    M * (Finset.filter (p ∣ ·) (Finset.Ico (n - n / M) n)).card + M ≥ n / p := by  have h1 : (Finset.filter (p ∣ ·) (Finset.Ico (n - n / M) n)).card ≥ (n / M) / p := by    have hsup : Finset.filter (p ∣ ·) (Finset.Ico (n - n / M) n) ⊇        Finset.image (p * ·) (Finset.Ico ((n - n / M + p - 1) / p)          ((n + p - 1) / p)) := fun _ hx ↦ by      simp +zetaDelta only [gt_iff_lt, mem_image, Finset.mem_Ico, Finset.mem_filter,        tsub_le_iff_right] at *      obtain ⟨a, ⟨ha₁, ha₂⟩, rfl⟩ := hx      refine ⟨⟨?_, ?_⟩, by norm_num⟩      · nlinarith [div_add_mod (n - n / M + p - 1) p, mod_lt (n - n / M + p - 1) hp,          Nat.sub_add_cancel (div_le_self n M), Nat.sub_add_cancel (succ_le_of_lt (by omega :            0 < n - n / M + p))]      · nlinarith [div_mul_le_self (n + p - 1) p, Nat.sub_add_cancel (by omega : 1 ≤ n + p)]    refine le_trans ?_ (Finset.card_mono hsup)    rw [Finset.card_image_of_injective _ fun _ _ h ↦ mul_left_cancel₀ hp.ne' h]    simp +arith only [card_Ico, div_le_iff_le_mul_add_pred hp]    zify    repeat rw [Nat.cast_sub] <;> push_cast <;> try omega    · nlinarith [Int.mul_ediv_add_emod (n + p - 1) p,        Int.emod_nonneg (n + p - 1) (by omega : (p : ℤ) ≠ 0),        Int.emod_lt_of_pos (n + p - 1) (by omega : (p : ℤ) > 0),        Int.mul_ediv_add_emod (p + (n - n / M) - 1) p,        Int.emod_nonneg (p + (n - n / M) - 1) (by omega : (p : ℤ) ≠ 0),        Int.emod_lt_of_pos (p + (n - n / M) - 1) (by omega : (p : ℤ) > 0),        div_mul_le_self n M]    · exact div_le_self _ _    · rw [div_le_iff_le_mul_add_pred hp]      rcases p with _ | _ | p <;> simp_all [succ_mul]      nlinarith [div_add_mod (n + (p + 1)) (p + 1 + 1), mod_lt (n + (p + 1)) (by omega :        p + 1 + 1 > 0), sub_le n (n / M), div_mul_le_self n M]  have h2 : n / p ≤ M * ((n / M) / p) + M := le_of_lt_succ (Nat.div_lt_of_lt_mul <| by    nlinarith [div_add_mod n M, mod_lt n hM, div_add_mod (n / M) p, mod_lt (n / M) hp])  exact h2.trans (by gcongr)