proposition: Lemma skipn_all : forall T n (a : list T), length a <= n -> skipn n a = nil.
proof: Proof. induction n; destruct a; simpl in *; intros; auto. exfalso; lia. apply IHn; lia. Qed.
imports: Coq.Lists.List Coq.ZArith.ZArith Coq.micromega.Lia