proposition: Lemma pow1_plus: forall {T} x y (c:T), pow1 c x ++ pow1 c y = pow1 c (x + y).
proof: Proof. induction x; intros. - simpl. reflexivity. - simpl. rewrite IHx. reflexivity. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List