coq - `0 1的更简单证明
我想知道该陈述的更短或更简单的证明`forall a:nat, 0 < a -> 1 < a + 1`。在 mathcomp/ssreflect 中。

我有以下证明，但希望存在更优雅的证明。

`From mathcomp Require Import all_ssreflect. Goal fora`

Question

我想知道该陈述的更短或更简单的证明forall a:nat, 0 < a -> 1 < a + 1。在 mathcomp/ssreflect 中。

我有以下证明，但希望存在更优雅的证明。

From mathcomp Require Import all_ssreflect.
Goal forall a:nat, 0 < a -> 1 < a + 1.
  move=>a.
  have H:1=0+1 by [].
  by rewrite {2}H ltn_add2r.
Qed.

score 3 · Accepted Answer

这个如何：

From mathcomp Require Import all_ssreflect.
Goal forall a:nat, 0 < a -> 1 < a + 1.
by move=>?; rewrite addn1 ltnS.
Qed.

coq - `0 1的更简单证明 我想知道该陈述的更短或更简单的证明forall a:nat, 0 < a -> 1 < a + 1。在 mathcomp/ssreflect 中。 我有以下证明，但希望存在更优雅的证明。