On Well Founded sets and the Axiom of Choice

First, build a context with classical logic and assume the Axiom of Functional Choice:
Require Import Classical.

Axiom functional_choice : forall (A:Set)(S:A->A->Prop), 
                      (forall x, exists y, S x y )-> 
                          exists f, forall x, S x (f x).
Prove the following theorem:
notWellFounded_seq
     : forall (A : Set) (R : A -> A -> Prop),
       ~ well_founded R ->
       exists f : nat -> A, (forall n : nat, R (f (S n)) (f n))

Remarks

Look also at that exercise
The Axiom of Functional Choice is presented on Coq's FAQ (in Coq's documentation ). Look at the section "The Logic of Coq : Axioms".

Solution

Look at this file .
Going home