I think of it as an alternative presentation of the same idea of induction. “Hey 2 * 3 * 4 * 5 looks like 2 * product [3, 4, 5]” is exemplifiying the induction proof underneath.
While we are at it, shameless plug of how I do it. To be fair, my students are 2nd/3rd year and have seen even “prove this inequality containing unknown constants, during the proof discover good values for the constants”, so it is a bit more believable that you can discover code during the proof too. To be fair^2, even 50yos fear recursion as much as total newbies do.
To be sure, I got from Graham Hutton, maybe also Ralf Hinze and Richard Bird etc., the idea of starting the proof first and letting the code emerge later.
On exams, I legit give hints like “Notice product [2, 3, 4, 5] = 2 * 3 * 4 * 5 = 2 * product [3, 4, 5] hint hint wink wink”, albeit for tougher questions than product.