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