Est-il possible de recurse conjointement sur une paire de variables en Coq?

Question

Disons que je suis en train de prouver ce qui suit:

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

Je me sens comme il pourrait être productif de réaliser l'induction sur la paire (n, m). Les cas seraient quelque chose comme (0, 0), (0, S m'), (S n', 0), et (S n', S m'). Est-ce possible?

Answer 1

Vous pouvez jeter un oeil à this answer pour avoir un aperçu de la commande lexicographique, mais je suggère de lire les commentaires @ejgallego, avec lesquels je suis totalement d'accord.