convert Nat.div_mul_le_self _ _ using 1
case h
r : Range
⊢ (r.stop - r.start + r.step - 1) / r.step * r.step ≤ r.stop + r.step - (r.start + 1)
case h.e'_4
r : Range
⊢ r.stop + r.step - (r.start + 1) = r.stop - r.start + r.step - 1