rw [build_s_polynomial]
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial p q ∈ ideal
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
p : Polynomial n ord
h_in_p : p ∈ ideal
q : Polynomial n ord
h_in_q : q ∈ ideal
⊢ build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt p) * p -
      build_s_polynomial.div_lcm_lt (build_s_polynomial.lcm p q) (Polynomial.lt q) * q ∈
    ideal