I had difficulty explaining Nat.below and Nat.brecOn in Section Structural Recursion and Induction of Theorem Proving in Lean 4. Sadly, I'll have to record a video of myself doing it again because my explanation missed the point. Still, I'm glad that I understood course-of-values recursion so much better than I did four years ago.

I was able to prove that the definition of the Fibonacci function, which directly uses Nat.brecOn, is equivalent to the one that doesn't.

• Section Structural Recursion and Induction of Theorem Proving in Lean 4: https://lean-lang.org/theorem_proving_in_lean4//Induction-and-Recursion/#structural-recursion-and-induction
• My proof: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/using.20Nat.2EbrecOn.20to.20define.20the.20fibonacci.20function/near/571451010