simp [Polynomial.Lt, Polynomial.lt, not_empty]
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Polynomial.lt p) (Polynomial.lt (p - Polynomial.Lt p)) == Ordering.lt) = true
n : ℕ
ord : Type
inst✝ : MonomialOrder (Variables n ord)
p : Polynomial n ord
not_empty : Std.RBSet.isEmpty p = false
⊢ (m_cmp (Std.RBSet.min! p)
        (if Std.RBSet.isEmpty (p - Polynomial.single (Std.RBSet.min! p)) = false then
          Std.RBSet.min! (p - Polynomial.single (Std.RBSet.min! p))
        else (1, get_variables n)) ==
      Ordering.lt) =
    true