Search code examples
coqssreflect

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

I want to know a shorter or simpler proof of the statement forall a:nat, 0 < a -> 1 < a + 1. in mathcomp/ssreflect.

I have the following proof but expect the existence of more elegant one.

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.
Solution

  • What about this one:

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