proposition: Lemma sum_app : forall (l1 l2:list int), sum (l1 ++ l2) = sum l1 + sum l2.
proof: Proof. Proof using. induction l1; intros l2; unfold sum; rew_listx*. rewrite* IHl1. unfold sum. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)