Coqの変数のペアで共同で再帰することは可能ですか？

Question

のは、私は、次のことを証明しようとしているとしましょう：

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

ペア(n, m)に誘導を行うために生産的であるかもしれないように私は感じます。その場合は、(0, 0),(0, S m'),(S n', 0など）、(S n', S m')のようなものになります。これはすべて可能ですか？

Answer 1

辞書型の順序を垣間見るにはthis answerを見ることができますが、私は完全に同意する@ejgallegoのコメントを読むことをお勧めします。