proposition: Lemma arith_sum_S n : arith_sum (S n) = arith_sum n + S n.
proof: Proof. unfold arith_sum. replace (S n * (S (S n))) with (2 * (S n) + n * (S n)). rewrite div2_add_double; lia. rewrite (Nat.mul_comm _ (S (S n))); simpl; lia. Qed.
imports: NPeano Arith micromega.Lia Setoid HahnBase