The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Pierre Casteran wrote:

>  Your proof of transitivity can be done if you first prove (or admit) 
> a little lemma
>
> (I hope it's true).
> Lemma lt_plus_ab : forall n a b : nat, n < a + b ->
>                              n < a \/ exists y, n=a+y /\ y < b.
> Admitted.
Require Import Peano_dec.
Require Import Omega.
Lemma lt_plus_ab : forall n a b : nat, n < a + b ->
                             n < a \/ exists y, n=a+y /\ y < b.
intros n a b; case (le_lt_dec a n).
intros.
right;exists (n-a).
 omega.
auto.
Qed.