proposition: Lemma nth_select2: forall {A:Type} (n:nat) (l:list A) , n >= length l <=> select n l= None.
proof: Proof. induction n as [|n Hind]; destruct l; allsimpl; try (split;sp;omega;fail). split;intro H. apply Hind; auto. omega. apply Hind in H; auto. omega. Qed.
imports: UsefulTypes bin_rels Omega