proposition: Theorem list_skipn_overflow : ∀ A n (cl : list A), length cl ≤ n → List.skipn n cl = [].
proof: Proof. intros A n cl H. revert n H. induction cl as [| c]; intros. rewrite list_skipn_nil; reflexivity. destruct n; [ exfalso; simpl in H; fast_omega H | simpl ]. apply IHcl, le_S_n; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz