proposition: Lemma arith_sum_inj_gen n n' (Ln: n' <= n) m m' (Lm: m' <= m) (EQ: arith_sum n + n' = arith_sum m + m') : n = 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