Используйте 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

Определенно есть несколько способов сделать это, и это не очень трудная цель, если вы используете некоторые существующие леммы.