Using gas instead of well-founded recursion is fine and preserves the original intent of the problem. But using recursors (nat.rec_on, etc.) directly is not idiomatic in Lean (or in any other theorem prover as far as I know). Using the equation compiler even for structural recursion makes a difference in Lean because it causes equational lemmas to be generated.