Докажите, что n <m + n или 0 <m в COQ

Question

Я пытаюсь использовать лемму для большего доказательства, но я не могу найти способ доказать одну из этих двух вещей. Кто-нибудь может мне помочь? Вот доказательство на данный момент:

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.

Answer 1

Ваше утверждение не может быть доказано, потому что оно не выполняется. Например, если мы берем n = m = p = 0, это подразумевает 0 < 0, явное противоречие.