Erdos392.Params.initial.balance_large_prime_le

@[blueprint  "initial-factorization-large-prime-le"  (statement := /-- A large prime $p \geq n/L$ cannot be in surplus. -/)  (proof := /-- No such prime can be present in the factorization.-/)  (latexEnv := "sublemma")]theorem Params.initial.balance_large_prime_le (P : Params) {p : ℕ} (hp : p ≥ P.n / P.L) :    P.initial.balance p ≤ 0 := by  simp only [Factorization.balance, Factorization.sum, initial, sub_nonpos]  have : (map (fun m ↦ m.factorization p)      (filter (fun m ↦ m ∈ (P.n / P.L).smoothNumbers)      (replicate P.M (Multiset.Ico (P.n - P.n / P.M) P.n)).join)).sum = 0 :=    sum_eq_zero fun x hx ↦ by      simp only [Multiset.mem_map, Multiset.mem_filter] at hx      obtain ⟨m, ⟨_, hsmooth⟩, rfl⟩ := hx      rw [factorization_eq_zero_iff]      rw [mem_smoothNumbers'] at hsmooth      grind  simp [this]