R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q✝ p q : R[X]
hq : Monic q
✝ : Nontrivial R
⊢ degree (p %ₘ q) ≤ degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q✝ p q : R[X]
hq : Monic q
⊢ degree (p %ₘ q) ≤ degree q
nontriviality R
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q✝ p q : R[X]
hq : Monic q
✝ : Nontrivial R
⊢ degree (p %ₘ q) ≤ degree q
exact (degree_modByMonic_lt _ hq).le