rintro ⟨h₁, h₂⟩
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
⊢ p ∧ a < b → p ∧ zToR a < zToR b
case intro
α : Type
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
p : Prop
a b : ℤ
h₁ : p
h₂ : a < b
⊢ p ∧ zToR a < zToR b