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
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
⊢ a / c ≤ b / c
a b c : Nat
hab : a ≤ b
hlt : b / c < a / c
this : c > 0
⊢ a / c ≤ b / c