是否可以在 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 cmets，我完全同意。