case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ natDegree ((comp p^[Nat.zero]) q) = natDegree p ^ Nat.zero * natDegree q

case succ
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
k : ℕ
IH : natDegree ((comp p^[k]) q) = natDegree p ^ k * natDegree q
⊢ natDegree ((comp p^[Nat.succ k]) q) = natDegree p ^ Nat.succ k * natDegree q
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
k : ℕ
⊢ natDegree ((comp p^[k]) q) = natDegree p ^ k * natDegree q
induction' k with k IH
no goals
case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ natDegree ((comp p^[Nat.zero]) q) = natDegree p ^ Nat.zero * natDegree q
simp
no goals
case succ
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
k : ℕ
IH : natDegree ((comp p^[k]) q) = natDegree p ^ k * natDegree q
⊢ natDegree ((comp p^[Nat.succ k]) q) = natDegree p ^ Nat.succ k * natDegree q
rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ, mul_assoc]