Finiteness, infinity and classical logic

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

Require Import Coinduc.

Require Import Classical.

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

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

The solution

Going home

Pierre Castéran