Theorem: Smt.Reconstruct.Arith.castLE' (Smt/Reconstruct/Arith/TightBounds/Lemmas.lean)

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ∀ {a b : ℤ}, a ≤ b → ↑a ≤ ↑b
Tactic:
simp
State after:
no goals