Valuation eval Int le pow

theorem valuation_evalInt_le_pow (q : k) (hq : valuation k q < 1) {F : ℤ⟦X⟧}    {M : ℕ} (hF : ∀ m < M, PowerSeries.coeff m F = 0) :    valuation k (evalInt q F) ≤ valuation k q ^ M := by  by_contra hlt  rw [not_le] at hlt  -- the partial sums satisfy the bound  have hpart : ∀ s : Finset ℕ,      valuation k (∑ n ∈ s, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) ≤        valuation k q ^ M := by    intro s    refine Valuation.map_sum_le _ fun n _ ↦ ?_    rcases lt_or_ge n M with h | h    · simp [hF n h]    · rw [map_mul, map_pow]      calc valuation k ((PowerSeries.coeff n F : ℤ) : k) * valuation k q ^ n          ≤ 1 * valuation k q ^ n := mul_le_mul_left (valuation_intCast_le_one _) _        _ = valuation k q ^ n := one_mul _        _ ≤ valuation k q ^ M := pow_le_pow_right_of_le_one' hq.le h  -- some partial sum is closer to the limit than `v(evalInt q F)`  have hS : HasSum (fun n : ℕ ↦ ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) (evalInt q F) :=    (summable_evalInt q hq F).hasSum  simp only [HasSum, SummationFilter.unconditional_filter,    (IsValuativeTopology.hasBasis_nhds (evalInt q F)).tendsto_right_iff] at hS  obtain ⟨s, hs⟩ :=    (hS (Units.mk0 _ (ne_of_gt (lt_of_le_of_lt zero_le hlt))) trivial).exists  simp only [Set.mem_setOf_eq] at hs  refine absurd ?_ (lt_irrefl (valuation k (evalInt q F)))  calc valuation k (evalInt q F)      = valuation k ((∑ n ∈ s, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) -          ((∑ n ∈ s, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) - evalInt q F)) := by        rw [sub_sub_cancel]    _ ≤ max (valuation k (∑ n ∈ s, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n))          (valuation k ((∑ n ∈ s, ((PowerSeries.coeff n F : ℤ) : k) * q ^ n) -            evalInt q F)) := Valuation.map_sub _ _ _    _ < valuation k (evalInt q F) := max_lt (lt_of_le_of_lt (hpart s) hlt) hs