proposition: Lemma sum_cons : forall (l:list int) (x:int), sum (x::l) = x + sum l.
proof: Proof. Proof using. rew_listx*. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)