proposition: Lemma arith_sum_lt n m (L : n < m) : arith_sum n + n < arith_sum m.
proof: Proof. apply le_plus_minus in L; rewrite L; clear L; generalize (m - S n) as k; intros. replace (S n + k) with (S (n + k)) by done. rewrite arith_sum_S. forward apply (arith_sum_le_mono n (n + k)); lia. Qed.
imports: NPeano Arith micromega.Lia Setoid HahnBase