The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Here is an attempt but I reach something wrong. Are you sure about
this statement?

Require Import Ring.
Require Import Arith.

Inductive w: nat -> nat -> Prop :=
 | C0: w 0 1
 | CS : forall n x y, w n y -> n*x = (S n)*y+1 -> w (S n) x.

Lemma foo: forall n, w n (2 * n + 1).
Proof.
  induction n.
  - constructor.
  - simpl in *.
    eapply CS.
    apply IHn.
    ring_simplify.
    (* wrong *)


2014-10-02 17:35 GMT+02:00 Christophe Bal 
<projetmbc AT gmail.com>:
> 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