case h.succ
p : ℕ
R : Type u_1
S : Type ?u.163480
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (↑(teichmuller p) 0) (Nat.succ n✝) = 0
case h.succ
p : ℕ
R : Type u_1
S : Type ?u.163480
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (↑(teichmuller p) 0) (Nat.succ n✝) = coeff 0 (Nat.succ n✝)
rw [zero_coeff]
no goals
case h.succ
p : ℕ
R : Type u_1
S : Type ?u.163480
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (↑(teichmuller p) 0) (Nat.succ n✝) = 0
rfl