simp [Nat.not_lt_zero start]
case neg
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
h : ¬stop = 0
⊢ (if hlt : start < 0 then
      match 0 with
      | 0 => pure init
      | Nat.succ i' =>
        let_fun this := ⋯;
        do
        let __do_lift ← f init #[][start]
        foldlM.loop f #[] 0 ⋯ i' (start + 1) __do_lift
    else pure init) =
    init
no goals