R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : degree q ≤ degree p
this : degree (p % q) < degree (q * (p / q))
⊢ degree q + degree (p / q) = degree p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : degree q ≤ degree p
⊢ degree q + degree (p / q) = degree p
have : degree (p % q) < degree (q * (p / q)) :=
  calc
    degree (p % q) < degree q := EuclideanDomain.mod_lt _ hq0
    _ ≤ _ := degree_le_mul_left _ (mt (div_eq_zero_iff hq0).1 (not_lt_of_ge hpq))
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : degree q ≤ degree p
this : degree (p % q) < degree (q * (p / q))
⊢ degree q + degree (p / q) = degree p
conv_rhs =>
  rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]