Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Recurrent sequence and unrecurrent formula

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Recurrent sequence and unrecurrent formula


Chronological Thread 
  • From: Christophe Bal <projetmbc AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Recurrent sequence and unrecurrent formula
  • Date: Thu, 2 Oct 2014 17:35:14 +0200

Hello.

Sorry for this very low level question (I still not found the time to learn seriously Coq).

Let's consider the sequence defined by  n w_n = (n + 1)w_{n-1} + 1  with the initial condition  w_0 = 1 .

How can I verify the validity of  w_n = 2 n + 1 ?

Christophe



Archive powered by MHonArc 2.6.18.

Top of Page