intros n r1 r2
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
⊢ ∀ (a : ℕ) (b₁_1 b₂ : R),
    single (a₁ + a) (b₁ * (↑φ)^[a₁] (b₁_1 + b₂)) =
      single (a₁ + a) (b₁ * (↑φ)^[a₁] b₁_1) + single (a₁ + a) (b₁ * (↑φ)^[a₁] b₂)
case e_g.h.h.h_add
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
a₁ : ℕ
b₁ : R
n : ℕ
r1 r2 : R
⊢ single (a₁ + n) (b₁ * (↑φ)^[a₁] (r1 + r2)) = single (a₁ + n) (b₁ * (↑φ)^[a₁] r1) + single (a₁ + n) (b₁ * (↑φ)^[a₁] r2)