proposition: Theorem sum_closed_form : forall n:nat, 2 * sum_n n = n * S n.
proof: Proof. induction n as [ | p IHp]. - reflexivity. - simpl sum_n. ring_simplify in IHp; ring_simplify. rewrite IHp;ring. Qed.
imports: Arith ArithRing