zify [add_le_add hP hQ, hP, hQ]
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p✝ q✝ : MvPolynomial ι S
hp : ¬p✝ = 0
hq : ¬q✝ = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p✝.support ∧ a.2 ∈ q✝.support
j : ι
f s p q fs ss : ℕ
hP : fs ≤ p
hQ : ss ≤ q
⊢ f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p✝ q✝ : MvPolynomial ι S
hp : ¬p✝ = 0
hq : ¬q✝ = 0
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p✝.support ∧ a.2 ∈ q✝.support
j : ι
f s p q fs ss : ℕ
hP : fs ≤ p
hQ : ss ≤ q
⊢ ↑f + ↑s + (↑p + ↑q - (↑fs + ↑ss)) = ↑f + (↑p - ↑fs) + (↑s + (↑q - ↑ss))