proposition: Lemma arith_sum_inj n m (EQ: arith_sum n = arith_sum m) : n = m.
proof: Proof. destruct (lt_eq_lt_dec n m) as [[A|A]|A]; desf; try lia. all: apply arith_sum_lt in A; lia. Qed.
imports: NPeano Arith micromega.Lia Setoid HahnBase