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