proposition: Lemma Finite_Empty_or_not A : Finite A -> (A->False) \/ exists a:A,True.
proof: Proof. intros (l,F). destruct l as [|a l]. - left; exact F. - right; now exists a. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec