have r_eq: remainder = divisible - quotient
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder ∈ asIdeal dividers
case r_eq
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
⊢ remainder = divisible - quotient

n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible quotient remainder : Polynomial n ord
dividers : List (Polynomial n ord)
div_sum_r_eq_p : divisible = quotient + remainder
quotient_in_ideal : quotient ∈ asIdeal dividers
divisible_in_ideal : divisible ∈ asIdeal dividers
r_eq : remainder = divisible - quotient
⊢ remainder ∈ asIdeal dividers