# On the sum of the *n* first natural numbers

We define the sum of naturals numbers from *1* upto
*n* with the following function :
Require Arith.
Fixpoint sum_n (n:nat) : nat :=
match n with O => O
| (S p) => (plus (S p) (sum_n p)) end.

Show that for each *n*, we have:

`2(sum `*n*)=*n(n+1)*

*n* <= sum_n *n*`.
`## Solution

Look at this file

Going home

Pierre Castéran