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
h : a * b < a * c
⊢ b < c
no goals