On verifying that primitive-recursive functions are provably total in PA

As far as I see, the book doesn't state or prove that primitive-recursive functions are provably total in PA; but most of the ingredients are there! The only thing missing is an explanation that Peano arithmetic proves that one can append elements to lists (coded via the beta function as numbers). I'd like to write a remark sketching that argument. Is there interest in that?

There is, however, a slight problem. The construction given in the proof of the beta function lemma uses the factorial function. I don't know how to verify in a non-circular fashion that the factorial function is total. I'd therefore change j! to lcm(1,...,j). Unlike the factorial function, the function j \mapsto lcm(1,...,j) can be represented and verified to be total without recourse to the beta function. The rest of the proof can be adapted to this change with extremely minimal effort. Am I missing something? Should I go ahead with the change?

Start by reviewing the book's beta function lemma and its use of the factorial function. Compare the proposed lcm(1,...,j) replacement and ensure the added remark explains, without circularity, that primitive-recursive functions are provably total in PA; done means the argument is complete and consistent with the existing proof.