We present a graded modal type theory with recursion over natural numbers and prove formally in Agda that it handles resources correctly, in the sense that an abstract machine accesses resources the “correct” number of times. The theory is parametrized, and can for instance be instantiated with modalities for erasure, linear types, or affine types among others. Compared to previous work, our eliminator for natural numbers is more flexible in the sense that it enables different resource-usage patterns. The correctness proof shows that our usage counting is sound and we also argue that it is accurate in the sense that it does not over approximate uses. We expect that the principles underlying the usage counting can be applied to eliminators of other inductive data types. The eliminator is demonstrated to be practical in the sense that it can be used both to define functions over natural numbers with expected usage counts of its arguments and that it can be used to encode other data types. Finally, we adapt our resource correctness proof to show correctness also for information flow instances in the form of a non-interference property.