start stop step : Nat
h : { start := start, stop := stop, step := step }.stop ≤ { start := start, stop := stop, step := step }.start
⊢ (if step = 0 then if stop ≤ start then 0 else stop else (stop - start + step - 1) / step) = 0
start stop step : Nat
h : { start := start, stop := stop, step := step }.stop ≤ { start := start, stop := stop, step := step }.start
⊢ numElems { start := start, stop := stop, step := step } = 0
simp [numElems]
case inr
start stop step : Nat
h : stop ≤ start
h✝ : ¬step = 0
⊢ (stop - start + step - 1) / step = 0
start stop step : Nat
h : { start := start, stop := stop, step := step }.stop ≤ { start := start, stop := stop, step := step }.start
⊢ (if step = 0 then if stop ≤ start then 0 else stop else (stop - start + step - 1) / step) = 0
split <;> simp_all
case inr.h₀
start stop step : Nat
h : stop ≤ start
h✝ : ¬step = 0
⊢ stop - start + step - 1 < step
case inr
start stop step : Nat
h : stop ≤ start
h✝ : ¬step = 0
⊢ (stop - start + step - 1) / step = 0
apply Nat.div_eq_of_lt
case inr.h₀
start stop step : Nat
h : stop ≤ start
h✝ : ¬step = 0
⊢ step - 1 < step
case inr.h₀
start stop step : Nat
h : stop ≤ start
h✝ : ¬step = 0
⊢ stop - start + step - 1 < step
simp [Nat.sub_eq_zero_of_le h]
no goals
case inr.h₀
start stop step : Nat
h : stop ≤ start
h✝ : ¬step = 0
⊢ step - 1 < step
exact Nat.pred_lt ‹_›