rw [‹n+1-k-1=n-k›, ‹succ (n-k-1)=n-k›]
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n + 1 - k - 1) x >>= foldM.loop f (n + 1) k) = fun x =>
    f (succ (n - k - 1)) x >>= foldM.loop (f ∘ succ) n k
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
h_ind : k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
hk : succ k ≤ n
this✝ : n + 1 - k - 1 = n - k
this : succ (n - k - 1) = n - k
⊢ (fun x => f (n - k) x >>= foldM.loop f (n + 1) k) = fun x => f (n - k) x >>= foldM.loop (f ∘ succ) n k