coq - Coq を使用して相対数の差を証明する

Question

forall m n : Z, m < n -> m -n < OCoq でどのように証明しますか? どうもありがとう！

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

それを行う方法は間違いなく複数あり、既存の補題を使用すればそれほど難しい目標ではありません。