intros p h_in_p q h_in_q
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
ideal : Ideal (Polynomial n ord)
⊢ ∀ (p : Polynomial n ord), p ∈ ideal → ∀ (q : Polynomial n ord), 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 p q ∈ ideal