case succ k h_ind =>
  dsimp [foldM.loop]
  have := calc
    n+1-k-1 = n.succ - k.succ := by simp only [Nat.sub_sub]
    _       = n-k := Nat.succ_sub_succ ..
  have := calc
    succ (n-k-1) = n-k-1+1 := rfl
    _            = n-k := Nat.sub_add_cancel (Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ hk))
  rw [‹n+1-k-1=n-k›, ‹succ (n-k-1)=n-k›]
  rw [h_ind (Nat.le_of_succ_le hk)]
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
⊢ foldM.loop f (n + 1) (succ k) = foldM.loop (f ∘ succ) n (succ k)
no goals