R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.5885
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : ¬i ∈ support p
⊢ ¬coeffIntegerNormalization M p i ≠ 0
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.5885
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : coeffIntegerNormalization M p i ≠ 0
⊢ i ∈ support p
contrapose h
no goals
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.5885
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : ¬i ∈ support p
⊢ ¬coeffIntegerNormalization M p i ≠ 0
rw [Ne.def, Classical.not_not, coeffIntegerNormalization, dif_neg h]