exact hp totalDegree_zero
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
q : MvPolynomial ι S
hq : ¬q.totalDegree = 0
hp : ¬totalDegree 0 = 0
⊢ False
no goals