∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {R : Type u_1}
  [inst_3 : AddCommGroup R] (a b : Lex (HahnSeries (FiniteArchimedeanClass M) R)), a + b = b + a