证明 COQ 中 n < m + n 或 0 < m

【问题标题】：Prove that n < m + n or that 0 < m in COQ证明 COQ 中 n < m + n 或 0 < m
【发布时间】：2018-06-30 17:33:11
【问题描述】：

我正在尝试使用引理来获得更大的证明，但我找不到证明这两件事之一的方法。有人可以帮助我吗？这是迄今为止的证明：

Lemma less_r : (forall m n p : nat, n + m < p + n + m).

Proof.
 intros.
 apply PeanoNat.Nat.add_lt_mono_r.
 apply PeanoNat.Nat.lt_add_pos_l.
 admit.
Qed.

【问题讨论】：

标签： coq proof inequality

【解决方案1】：

你的陈述不能被证明，因为它不成立。例如，如果我们取n = m = p = 0，它暗示0 < 0，显然矛盾。

【讨论】：

但是没有办法证明这一点，除了 0
@RafaelSantos 我不明白你的意思。如果你想证明它，你需要修改你的陈述。一种可能性是添加一个关于p 的前提条件：forall n m p, 0 < p -> n + m < p + n + m，您可以使用omega 策略轻松证明这一点（在您的文件中添加Require Import Omega. 之后）。但我不知道这个引理是否适合您的需求。
所以为了让我们了解你想要做什么，你想让 coq 反驳你的说法？