CODEWITHSUNDEEP
coqssreflect
Teirflegne
Teirflegne

Reputation: 99

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.

Upvotes: 2

Views: 94

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23612

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.

Upvotes: 3

Related Questions