Would that call for replacing that function with some kind of inductive abstraction to help it see that it generalizes to N byte numbers?