Definition f1 (x:nat): nat := let y:=x+1 in y*y-x*x.
Definition f2 (x: nat): nat := x+x+1.
Compute f1 3.
Compute f1 8.
Compute f1 13.