Theorem: Int.mul_lt_mul_left (Smt/Reconstruct/Int/Lemmas.lean)

State before:
c x y : Int
hc : c > 0
⊢ (c * x < c * y) = (x < y)
Tactic:
apply propext
State after:
case a
c x y : Int
hc : c > 0
⊢ c * x < c * y ↔ x < y

State before:
case a
c x y : Int
hc : c > 0
⊢ c * x < c * y ↔ x < y
Tactic:
constructor
State after:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x < c * y → x < y

case a.mpr
c x y : Int
hc : c > 0
⊢ x < y → c * x < c * y

State before:
case a.mp
c x y : Int
hc : c > 0
⊢ c * x < c * y → x < y
Tactic:
apply Int.lt_of_mul_lt_mul_left (h := Int.le_of_lt hc)
State after:
no goals

State before:
case a.mpr
c x y : Int
hc : c > 0
⊢ x < y → c * x < c * y
Tactic:
apply Int.mul_lt_mul_of_pos_left (h₂ := hc)
State after:
no goals