∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.ble b' = false → ¬a ≤ b