coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to prove this?

From: Sidi <Sidi.Ould_Biha AT inria.fr>
To: catty wang <catty.wang AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to prove this?
Date: Tue, 29 Jun 2010 14:23:05 +0800
Organization: INRIA

On Tue, 2010-06-29 at 13:52 +0800, catty wang wrote:
> hi,all:
>
>        I wondering how to prove this :
>                        forall x:nat, exists y:nat,y=x+2.
>        please help me,thanks .
>
>                                         catty.
>
Hi,
You can prove this lemma by induction x.

Goal forall x, exists y, y = x + 2.
induction x. exists 2; auto.
destruct IHx as [x' Exx']. exists (S x'). simpl. auto.

[Coq-Club] how to prove this?, catty wang
- Re: [Coq-Club] how to prove this?, Sidi
  - Re: [Coq-Club] how to prove this?, Jean-Francois Monin