proposition: Lemma list_sum_app : forall l1 l2, list_sum (l1 ++ l2) = list_sum l1 + list_sum l2.
proof: Proof. intro l1; induction l1 as [|a l1 IHl1]; intros l2; [ reflexivity | ]. simpl; rewrite IHl1. apply Nat.add_assoc. Qed.
imports: PeanoNat