pleasant afternoon doing some exercises in #lean4 proving tail-recursive forms of functions are equivalent to their non-tail-recursive counterparts