proposition: Lemma Fin_Finite n : Finite (Fin.t n).
proof: Proof. induction n as [|n IHn]. - exists nil. red;inversion 1. - destruct IHn as (l,Hl). exists (Fin.F1 :: map Fin.FS l). intros a. revert n a l Hl. refine (@Fin.caseS _ _ _); intros. + now left. + right. now apply in_map. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec