使用Coq來證明相對數之間的差異

Question

您如何證明：Coq中的forall m n : Z, m < n -> m -n < O？非常感謝！

Answer 1

如果你只關心證明它，而不是有關證明，只需使用歐米茄：

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 

肯定有這樣做的方法不止一種，如果你使用一些現有的引理它不是一個非常困難的目標。