Sep 30, 2023 Lean prover Proving Termination in Lean 4, pt. 1 Convince the prover that your function will terminate.