coq - 使用 Coq 证明相对数之间的差异

Question

你如何证明：forall m n : Z, m < n -> m -n < O在 Coq 中？非常感谢！

Answer 1

如果您只关心证明它，而不关心证明，只需使用 omega：

Require Import Omega.

Goal forall m n : Z, (m < n)%Z -> (m - n < 0%Z)%Z.
intros. omega.
Qed.

---

如果你必须在练习或家庭作业中证明这一点，如果你依赖一些现有的证明，这并不难。

例如，您可以组合这些家伙：

Zminus_diag_reverse
     : forall n : Z, 0%Z = (n - n)%Z

Zplus_lt_le_compat
     : forall n m p q : Z, (n < m)%Z -> (p <= q)%Z -> (n + p < m + q)%Z

肯定有不止一种方法可以做到，如果你使用一些现有的引理，这不是一个很难的目标。