dec f : num -> num;
--- f 0 <= 0;
--- f 1 <= 1;
--- f(n+2) <= f n + f(n+1);