sum-one-to-n Proof that the sum one to n is n*(n+1)/2 in Coq Contains a long proof sum_one_to_n_reduction and then a shorter proof sum_one_to_n_reduction' by using more omegas.