R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
⊢ order φ ≤ ↑n
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑n < order φ
⊢ ↑(coeff R n) φ = 0
contrapose! h
no goals
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
n : ℕ
h : ↑(coeff R n) φ ≠ 0
⊢ order φ ≤ ↑n
exact order_le _ h