Theorem: polynomial.div_sum_r_eq_p (Diploma/Polynomials/Division.lean)

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : (p == 0) = true
⊢ divisible = quotient + remainder
Tactic:
have eq_zero := beq_eq p h
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = p + quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder
Tactic:
rw [eq_zero, zero_add] at sum_eq
State after:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder

State before:
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
divisible p quotient remainder : Polynomial n ord
sum_eq : divisible = quotient + remainder
h : (p == 0) = true
eq_zero : p = 0
⊢ divisible = quotient + remainder
Tactic:
exact sum_eq
State after:
no goals