proposition: Lemma napp_plus: forall T (n m : nat) (l : list T), napp (n + m) l = napp n l ++ napp m l.
proof: Proof. intros T n m l. induction n as [|n IHn]. - reflexivity. - simpl. rewrite IHn, app_assoc. reflexivity. Qed.
imports: Coq(Lia)