`0<a -> 1<a+1` 的简单证明

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.

Answer 1

这个怎么样：

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

Simpler proof of `0<a -> 1<a+1`