Erdos392.Params.rough_valuation_eq_k_valuation

lemma Params.rough_valuation_eq_k_valuation (P : Params) (m : ℕ) (hm : m ∈ rough_set P)    (p : ℕ) (hp : p ≤ P.L) : m.factorization p = (rough_k P m).factorization p := by  set q := rough_q P m  set k := rough_k P m  have hp_ne_q : p ≠ q := by    have := rough_qk_prop P m hm    have := this.2.1    rw [ge_iff_le, Nat.div_le_iff_le_mul_add_pred] at this <;> norm_num at *    · have := P.hL'      rw [gt_iff_lt, Real.sqrt_lt] at this <;> norm_cast at * <;>        nlinarith [div_add_mod P.n P.L, mod_lt P.n P.hL_pos, P.hL]    · exact P.hL_pos  have := rough_qk_prop P m hm  rw [this.2.2.2.1, Nat.factorization_mul] <;> norm_num [this.1.ne_zero, hp_ne_q]  · simp +zetaDelta only [ne_eq, ge_iff_le, Nat.add_eq_right] at *    rw [this.1.factorization]    norm_num [hp_ne_q]  · exact Nat.ne_of_gt (Nat.pos_of_ne_zero fun h => by      have := this.2.2.2.1; simp_all +singlePass)