Is it possible to jointly recurse on a pair of variables in Coq?

Question

Let's say that I'm trying to prove the following:

Theorem le_s_n : forall n m, S n <= S m -> n <= m.

I feel like it might be productive to perform induction on the pair (n, m). The cases would be something like (0, 0), (0, S m'), (S n', 0), and (S n', S m'). Is this at all possible?

Answer 1

You could have a look at this answer to have a glimpse on lexicographic ordering, but I suggest to read @ejgallego comments, that I totally agree with.