simp [h]
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ foldlM.loop f #[] 0 ⋯ 0 start init = init