case inl hlt =>
  have : c > 0 := (Nat.lt_or_ge 0 c).elim id $ by
    intro h; cases h; rw [Nat.div_zero, Nat.div_zero] at hlt; cases hlt
  have := (Nat.div_lt_iff_lt_mul ‹c>0›).mp hlt
  have := calc
    b < a/c*c := this
    _ ≤ a := Nat.div_mul_le_self a c
    _ ≤ b := hab
  exact absurd this (Nat.lt_irrefl b)
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ a / c ≤ b / c
no goals