Theorem: Smt.Reconstruct.Arith.castGEZero (Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c : α
⊢ ∀ {a : ℤ}, a ≤ 0 → zToR a ≤ 0
Tactic:
simp
State after:
no goals