proposition: Lemma firstn_cons : forall T n a (b : list T), 0 < n -> firstn n (a :: b) = a :: firstn (n - 1) b.
proof: Proof. destruct n; intros. lia. simpl. replace (n - 0) with n; [ | lia ]. reflexivity. Qed.
imports: Coq.Lists.List Coq.ZArith.ZArith Coq.micromega.Lia