. intro h
  exact Nat.gt_of_not_le fun hle : c ≤ b =>
    have : a * c ≤ a * b := Nat.mul_le_mul_left a hle
    have : ¬ a * b < a * c := Nat.not_lt_of_le this
    absurd h this
case mp
a b c : Nat
h : 0 < a
⊢ a * b < a * c → b < c

case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c
case mpr
a b c : Nat
h : 0 < a
⊢ b < c → a * b < a * c