proposition: Lemma firstn_all : forall T n (a : list T), length a <= n -> firstn n a = a.
proof: Proof. induction n; destruct a; simpl; intros; auto. exfalso; lia. simpl. f_equal. eapply IHn; lia. Qed.
imports: Coq.Lists.List Coq.ZArith.ZArith Coq.micromega.Lia