sorry
case inl
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))) == Ordering.lt) = true

case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true
case inr
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
h✝ : ¬Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false
⊢ (m_cmp (Std.RBSet.min! p) (1, get_variables n) == Ordering.lt) = true