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