Finiteness, infinity and classical logic

Prove the following theorems ( You will need classical logic ! ).

Require Import chap13.

Require Import Classical.

Lemma Not_Infinite_Finite :
  forall (A:Type) (l:LList A),
   ~ Infinite l -> Finite l.

Lemma Finite_or_Infinite :
  forall (A:Type)(l:LList A), Finite l \/ Infinite l.

Remark

Notice that classical logic is really needed for proving Finite_or_Infinite. If this theorem were provable in intuitionnistic logic, we could infer an algorithm for deciding whether the computation of any Turing machine is finite.
The solution

Going home

Pierre Castéran