Require Import Arith ArithRing.
Ltac defn x := unfold x; fold x.
Fixpoint sum (n : nat) : nat :=
match n with
| O => O
| S n => S n + sum n
end.
Theorem sum_equals : forall n, 2 * sum n = n * (n + 1).
induction n.
trivial.
defn sum.
rewrite mult_plus_distr_l.
rewrite IHn.
ring_nat.
Qed.
Print sum_equals.