proposition: Lemma arith_sum_le_mono n m (L : n <= m) : arith_sum n <= arith_sum m.
proof: Proof. apply le_plus_minus in L; rewrite L; clear L; generalize (m - n) as k; ins. rewrite Nat.add_comm; induction k; ins. rewrite arith_sum_S; lia. Qed.
imports: NPeano Arith micromega.Lia Setoid HahnBase