Erdos392.Params.initial.count_multiples_le

lemma Params.initial.count_multiples_le (A B p : ℕ) (hp : p > 0) :    (Finset.filter (p ∣ ·) (Finset.Ico A B)).card ≤ (B - A + p - 1) / p := by  have hsub : Finset.filter (p ∣ ·) (.Ico A B) ⊆ image (p * ·) (.Ico ((A + p - 1) / p)      ((B + p - 1) / p)) := fun m hm ↦ by    obtain ⟨k, hk⟩ : ∃ k, m = p * k := by aesop    simp only [gt_iff_lt, Finset.mem_filter, Finset.mem_Ico, mem_image] at *    exact ⟨k, ⟨le_of_lt_succ <| Nat.div_lt_of_lt_mul <|      by rw [tsub_lt_iff_left] <;> grind,      lt_of_succ_le <| le_div_iff_mul_le hp |>.2 <|        by rw [Nat.le_sub_iff_add_le] <;> grind⟩, hk.symm⟩  refine (card_le_card hsub).trans ?_  norm_num [card_image_of_injective _ fun x y hxy ↦ mul_left_cancel₀ hp.ne' hxy, card_Ico]  rcases le_total B A with h | h <;> simp_all only [div_le_iff_le_mul_add_pred, tsub_le_iff_right]  · rcases p with _ | _ | p <;> simp_all +arith [Nat.div_eq_of_lt]    linarith [Nat.div_add_mod (A + p + 1) (p + 2), Nat.mod_lt (A + p + 1) (by grind : p + 2 > 0)]  · linarith [div_add_mod (B - A + p - 1) p, mod_lt (B - A + p - 1) hp,      div_add_mod (A + p - 1) p, mod_lt (A + p - 1) hp, Nat.sub_add_cancel h,      Nat.sub_add_cancel (by grind : 1 ≤ p), Nat.sub_add_cancel (by grind : 1 ≤ B - A + p),      Nat.sub_add_cancel (by grind : 1 ≤ A + p)]