Valuation eval Int sub sum le

theorem valuation_evalInt_sub_sum_le (q : k) (hq : valuation k q < 1)    (F : ℤ⟦X⟧) (N : ℕ) :    valuation k (evalInt q F -      ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) ≤    valuation k q ^ N := by  -- the partial sum is the evaluation of the truncation  have htrunc : evalInt q ((F.trunc N : Polynomial ℤ) : ℤ⟦X⟧) =      ∑ n ∈ Finset.range N, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n := by    have h0 : ∀ n ∉ Finset.range N,        ((PowerSeries.coeff n ((F.trunc N : Polynomial ℤ) : ℤ⟦X⟧) : ℤ) : k) * q ^ n = 0 := by      intro n hn      rw [Polynomial.coeff_coe, PowerSeries.coeff_trunc,        if_neg (by simpa using hn), Int.cast_zero, zero_mul]    refine (hasSum_sum_of_ne_finset_zero h0).tsum_eq.trans ?_    exact Finset.sum_congr rfl fun n hn ↦ by      rw [Polynomial.coeff_coe, PowerSeries.coeff_trunc, if_pos (Finset.mem_range.mp hn)]  rw [← htrunc, ← evalInt_sub (summable_evalInt q hq _) (summable_evalInt q hq _)]  refine valuation_evalInt_le_pow q hq fun m hm ↦ ?_  rw [map_sub, Polynomial.coeff_coe, PowerSeries.coeff_trunc, if_pos hm, sub_self]