proposition: Lemma pow_plus: forall T (n m : nat) (l : list T), pow l (n + m) = pow l n ++ pow l m.
proof: Proof. induction n; simpl; intros. - reflexivity. - simpl. rewrite IHn. repeat rewrite app_assoc. reflexivity. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List