case zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
⊢ natDegree (p ^ Nat.zero) ≤ Nat.zero * natDegree p

case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree (p ^ Nat.succ i) ≤ Nat.succ i * natDegree p
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
n : ℕ
⊢ natDegree (p ^ n) ≤ n * natDegree p
induction' n with i hi
no goals
case zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
⊢ natDegree (p ^ Nat.zero) ≤ Nat.zero * natDegree p
simp
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree (p * p ^ i) ≤ natDegree p + i * natDegree p
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree (p ^ Nat.succ i) ≤ Nat.succ i * natDegree p
rw [pow_succ, Nat.succ_mul, add_comm]
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree p + natDegree (p ^ i) ≤ natDegree p + i * natDegree p
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree (p * p ^ i) ≤ natDegree p + i * natDegree p
apply le_trans natDegree_mul_le
no goals
case succ
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q : R[X]
ι : Type ?u.695996
p : R[X]
i : ℕ
hi : natDegree (p ^ i) ≤ i * natDegree p
⊢ natDegree p + natDegree (p ^ i) ≤ natDegree p + i * natDegree p
exact add_le_add_left hi _