∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddMonoid (α i)]
  [inst_2 : (i : ι) → LinearOrder (α i)] [∀ (i : ι), AddRightStrictMono (α i)],
  AddRightStrictMono (Lex (Π₀ (i : ι), α i))