Require Export List ZArith Recdef.
Open Scope Z_scope.

Function sos (n:Z) {measure Zabs_nat} : Z :=
  if Z_le_dec n 0 then 0 else n^2 + sos (n-1).
intros n npos _.
SearchPattern (Zabs_nat _ < Zabs_nat _)%nat.
apply Zabs_nat_lt.
omega.
Defined.

Definition sample := 10 :: 100 :: 1000 ::nil.

Eval vm_compute in map sos sample.
Eval vm_compute in map (fun x => 3 * sos x) sample.
Eval vm_compute in map (fun x => 3 * sos x - x^3) sample.
Eval vm_compute in map (fun x => 2 * (3 * sos x - x^3)) sample.
Eval vm_compute in map (fun x => 2 * (3 * sos x - x ^ 3) - 3 * x ^ 2) sample.
Eval vm_compute in 
  map (fun x => 2 * (3 * sos x - x ^ 3) - 3 * x ^ 2  - x) sample.

Lemma sos_prop : forall x, 0<= x -> 6*sos x = 2 * x ^ 3 + 3 * x ^ 2 + x.
intros x.
functional induction sos x.
 intros npos.
 assert (n = 0) by omega. 
 subst n.
 ring.
intros npos.
replace (6 * (n ^ 2 + sos (n - 1))) with (6 * n ^ 2 + 6 * sos (n - 1)).
rewrite IHz.
ring.
omega.
ring.
Qed.