Erdos392.Params.rough_set_structure

lemma Params.rough_set_structure (P : Params) (m : ℕ) (hm : m ∈ rough_set P) :    ∃ q k, q.Prime ∧ q ≥ P.n / P.L ∧ k ≤ P.L ∧ m = q * k ∧ m.factorization q = 1 := by  obtain ⟨q, hq_prime, hq_ge, hq_div⟩ := exists_large_prime_of_rough P m hm  use q  have hk_le : m / q ≤ P.L := by    have h_div : m ≤ P.n - 1 :=      Nat.le_sub_one_of_lt (Finset.mem_Ico.mp (Finset.mem_filter.mp hm |>.1) |>.2)    have h_div' : m / q ≤ (P.n - 1) / q := Nat.div_le_div_right h_div    refine le_trans h_div' (Nat.le_of_lt_succ ?_)    rw [Nat.div_lt_iff_lt_mul hq_prime.pos, tsub_lt_iff_left] <;>      nlinarith [Nat.div_add_mod P.n P.L, Nat.mod_lt P.n P.hL_pos, P.hL]  refine ⟨m / q, hq_prime, hq_ge, hk_le, (Nat.mul_div_cancel' hq_div).symm, ?_⟩  have hm_pos : m ≠ 0 := by    intro h    simp only [h, rough_set, Finset.mem_filter, Finset.mem_Ico, nonpos_iff_eq_zero] at hm    have : P.n - P.n / P.M > 0 := Nat.sub_pos_of_lt (Nat.div_lt_self (by linarith) P.hM)    omega  exact valuation_eq_one_of_large_prime P m q    (Finset.mem_Ico.mp (Finset.mem_filter.mp hm |>.1) |>.2) hm_pos hq_prime hq_ge hq_div