exact hstop
case h.a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ stop ≤ start
no goals