[cheese_it]

But how do you know that induction is valid to use on natural numbers? It's because their definition/construction follows a set of rules that makes them inductive. Some languages like Coq make this explicit by providing an 'Inductive' keyword for defining inductive types.